Normalise type before checking it's a valid postulate
commit12189d73e7eab9422d52aa65bf325bc21671e910
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 18 Feb 2013, 20:08 (14 years ago)
parent2b09cc1
CHANGELOG+2
@@ -3,6 +3,8 @@ New in 0.9.7:
33
44User visible changes:
55
6+* Primitives for 8,16,32 and 64 bit integers
7+
68Internal changes:
79
810* 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
9292 [] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen!
9393 [ty] -> return ty
9494 ist <- getIState
95− let (ap, _) = unApply (getRetTy fty)
95+ let (ap, _) = unApply (getRetTy (normalise ctxt [] fty))
9696 logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)
9797 let postOK = case ap of
9898 P _ tn _ -> case lookupCtxt Nothing tn