git.iko.soy/Idris-dev
on master help sign in
Normalise type before checking it's a valid postulate
12189d7Edwin Brady
CHANGELOG+2
compare with master
unifiedsplit
@@ -3,6 +3,8 @@ New in 0.9.7:
3
3
4User visible changes:
4User visible changes:
5
5
6+* Primitives for 8,16,32 and 64 bit integers
7+
6Internal changes:
8Internal changes:
7
9
8* Change unification so that it keeps track of failed constraints in case
10* Change unification so that it keeps track of failed constraints in case
src/Idris/ElabDecls.hs+1−1
@@ -92,7 +92,7 @@ elabPostulate info syn doc fc opts n ty
92 [] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen!
92 [] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen!
93 [ty] -> return ty
93 [ty] -> return ty
94 ist <- getIState
94 ist <- getIState
95− let (ap, _) = unApply (getRetTy fty)
95+ let (ap, _) = unApply (getRetTy (normalise ctxt [] fty))
96 logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)
96 logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)
97 let postOK = case ap of
97 let postOK = case ap of
98 P _ tn _ -> case lookupCtxt Nothing tn
98 P _ tn _ -> case lookupCtxt Nothing tn