ucsd-progsys/liquidhaskell

Cannot parse the unit value in refinement bounds

Open

#1300 aperta il 17 apr 2018

Vedi su GitHub
 (1 commento) (0 reazioni) (0 assegnatari)Haskell (157 fork)batch import
easygood first issueparser

Metriche repository

Star
 (1306 star)
Metriche merge PR
 (Merge medio 2g 18h) (12 PR mergiate in 30 g)

Descrizione

I'm not really sure it's by design or not, LH fails to parse bounds which include the unit literal ().

{-@
    testee :: forall <
                p :: Int -> () -> Int -> Bool
              , q :: Int -> () -> Int -> Bool
              >.
              { n :: Int |- Int<p n ()> <: Int<q n ()> }
              Int
@-}
testee :: Int
testee = 42

Literals of the types other than () look okay, e.g. in the case of Int or Bool, the code is compilable.

{-@
    testee :: forall <
                p :: Int -> Int -> Int -> Bool
              , q :: Int -> Int -> Int -> Bool
              >.
              { n :: Int |- Int<p n 42> <: Int<q n 42> }
              Int
@-}
testee :: Int
testee = 42

Guida contributor

Direzione di ricerca
Ispeziona i file sorgente Haskell relativi all'analisi dei bounds di raffinamento in LiquidHaskell. Cerca dove viene analizzato il letterale unità `()` e confrontalo con come vengono gestiti altri letterali come `42`. Il problema è probabilmente nel parser o nel type checker per i tipi di raffinamento.
Tech stack
haskell
Dominio
compilers
Tipo issue
Bug
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-3 ore
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
Haskell
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
70