git.iko.soy/Idris-dev
on master help sign in
Don't normalise constructor types
cfc8436Edwin Brady
src/Idris/Coverage.hs+3−3
compare with master
unifiedsplit
@@ -340,9 +340,9 @@ checkAllCovering _ _ _ _ = return ()
340
340
341checkPositive :: [Name] -> (Name, Type) -> Idris Totality
341checkPositive :: [Name] -> (Name, Type) -> Idris Totality
342checkPositive mut_ns (cn, ty')
342checkPositive mut_ns (cn, ty')
343+ = do i <- getIState
343− = do let ty = delazy' True ty'
344+ let ty = delazy' True (normalise (tt_ctxt i) [] ty')
344 let p = cp ty
345 let p = cp ty
345− i <- getIState
346 let tot = if p then Total (args ty) else Partial NotPositive
346 let tot = if p then Total (args ty) else Partial NotPositive
347 let ctxt' = setTotal cn tot (tt_ctxt i)
347 let ctxt' = setTotal cn tot (tt_ctxt i)
348 putIState (i { tt_ctxt = ctxt' })
348 putIState (i { tt_ctxt = ctxt' })
@@ -597,7 +597,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
597 toJust (n, t) = Just t
597 toJust (n, t) = Just t
598
598
599 getType n = case lookupTy n (tt_ctxt ist) of
599 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
601
601
602 isInductive (P _ nty _) (P _ nty' _) =
602 isInductive (P _ nty _) (P _ nty' _) =
603 let co = case lookupCtxt nty (idris_datatypes ist) of
603 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
244
244
245 logElab 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t
245 logElab 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t
246 logElab 5 $ "Inaccessible args: " ++ show inacc
246 logElab 5 $ "Inaccessible args: " ++ show inacc
247− logElab 2 $ "---> " ++ show n ++ " : " ++ show cty'
247+ logElab 2 $ "---> " ++ show n ++ " : " ++ show cty
248
248
249 -- Add to the context (this is temporary, so that later constructors
249 -- Add to the context (this is temporary, so that later constructors
250 -- can be indexed by it)
250 -- can be indexed by it)
@@ -259,7 +259,7 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen
259 addIBC (IBCDoc n)
259 addIBC (IBCDoc n)
260 fputState (opt_inaccessible . ist_optimisation n) inacc
260 fputState (opt_inaccessible . ist_optimisation n) inacc
261 addIBC (IBCOpt n)
261 addIBC (IBCOpt n)
262− return (n, cty')
262+ return (n, cty)
263 where
263 where
264 tyIs con (Bind n b sc) = tyIs con (substV (P Bound n Erased) sc)
264 tyIs con (Bind n b sc) = tyIs con (substV (P Bound n Erased) sc)
265 tyIs con t | (P Bound n' _, _) <- unApply t
265 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
18 Parity (S (S (j + j)))
18 Parity (S (S (j + j)))
19
19
20Type mismatch between
20Type mismatch between
21− Parity (plus (S j) (S j)) (Type of Even)
21+ Parity (S j + S j) (Type of Even)
22and
22and
23 Parity (S (S (plus j j))) (Expected type)
23 Parity (S (S (plus j j))) (Expected type)
24
24