cfc8436 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Don't normalise constructor types

This is mainly to improve display of error messages and generation of patterns in 'with', since normalising leads to normalised patters, rather than the patters given in the constructor type.

commitcfc84363448f4d7894aa50b1708be510d02c7895 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 18 Feb 2016, 18:36 (11 years ago) parentdc7fd3b

3 files changed+6−6

compare with master

unifiedsplit

src/Idris/Coverage.hs+3−3 src/Idris/Elab/Data.hs+2−2 test/tutorial006/expected+1−1

src/Idris/Coverage.hs+3−3

@@ -340,9 +340,9 @@ checkAllCovering _ _ _ _ = return ()

340340

341341checkPositive :: [Name] -> (Name, Type) -> Idris Totality

342342checkPositive mut_ns (cn, ty')

343− = do let ty = delazy' True ty'

343+ = do i <- getIState

344+ let ty = delazy' True (normalise (tt_ctxt i) [] ty')

344345 let p = cp ty

345− i <- getIState

346346 let tot = if p then Total (args ty) else Partial NotPositive

347347 let ctxt' = setTotal cn tot (tt_ctxt i)

348348 putIState (i { tt_ctxt = ctxt' })

@@ -597,7 +597,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

597597 toJust (n, t) = Just t

598598

599599 getType n = case lookupTy n (tt_ctxt ist) of

600− [ty] -> delazy ty -- must exist

600+ [ty] -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist

601601

602602 isInductive (P _ nty _) (P _ nty' _) =

603603 let co = case lookupCtxt nty (idris_datatypes ist) of

src/Idris/Elab/Data.hs+2−2

@@ -244,7 +244,7 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

244244

245245 logElab 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t

246246 logElab 5 $ "Inaccessible args: " ++ show inacc

247− logElab 2 $ "---> " ++ show n ++ " : " ++ show cty'

247+ logElab 2 $ "---> " ++ show n ++ " : " ++ show cty

248248

249249 -- Add to the context (this is temporary, so that later constructors

250250 -- can be indexed by it)

@@ -259,7 +259,7 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

259259 addIBC (IBCDoc n)

260260 fputState (opt_inaccessible . ist_optimisation n) inacc

261261 addIBC (IBCOpt n)

262− return (n, cty')

262+ return (n, cty)

263263 where

264264 tyIs con (Bind n b sc) = tyIs con (substV (P Bound n Erased) sc)

265265 tyIs con t | (P Bound n' _, _) <- unApply t

test/tutorial006/expected+1−1

@@ -18,7 +18,7 @@ When checking right hand side of with block in Main.parity with expected type

1818 Parity (S (S (j + j)))

1919

2020Type mismatch between

21− Parity (plus (S j) (S j)) (Type of Even)

21+ Parity (S j + S j) (Type of Even)

2222and

2323 Parity (S (S (plus j j))) (Expected type)

2424