git.iko.soy/Idris-dev
on master help sign in
'compute' rather than whnf on disambiguation
25eea96Edwin Brady
src/Idris/Elab/Term.hs+2−2
compare with master
unifiedsplit
@@ -500,11 +500,11 @@ elab ist info emode opts fn tm
500 showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here
500 showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here
501
501
502 doPrune as =
502 doPrune as =
503− do whnf_compute -- to get 'Delayed' if it's there
503+ do compute -- to get 'Delayed' if it's there
504 ty <- goal
504 ty <- goal
505 ctxt <- get_context
505 ctxt <- get_context
506 env <- get_env
506 env <- get_env
507− let ty' = whnf ctxt env (unDelay ty)
507+ let ty' = unDelay ty
508 let (tc, _) = unApply ty'
508 let (tc, _) = unApply ty'
509 return $ pruneByType eimpossible env tc ty' ist as
509 return $ pruneByType eimpossible env tc ty' ist as
510
510
test/error005/expected+9−9
@@ -2,8 +2,8 @@ error005.idr:13:1:When checking right hand side of two with expected type
2 Fin 2
2 Fin 2
3
3
4When checking argument prf to function Data.Fin.fromInteger:
4When checking argument prf to function Data.Fin.fromInteger:
5− When using 2 as a literal for a Fin (fromIntegerNat 2)
5+ When using 2 as a literal for a Fin 2
6− 2 is not strictly less than fromIntegerNat 2
6+ 2 is not strictly less than 2
7error005.idr:16:1:When checking right hand side of hahaha with expected type
7error005.idr:16:1:When checking right hand side of hahaha with expected type
8 Fin n
8 Fin n
9
9
@@ -14,18 +14,18 @@ error005.idr:22:1:When checking right hand side of notOk with expected type
14 Fin (plus 2 n)
14 Fin (plus 2 n)
15
15
16When checking argument prf to function Data.Fin.fromInteger:
16When checking argument prf to function Data.Fin.fromInteger:
17− When using 2 as a literal for a Fin (plus (fromIntegerNat 2) n)
17+ When using 2 as a literal for a Fin (S (S n))
18− 2 is not strictly less than plus (fromIntegerNat 2) n
18+ 2 is not strictly less than S (S n)
19error005.idr:23:24:When checking right hand side of b0rken with expected type
19error005.idr:23:24:When checking right hand side of b0rken with expected type
20 Fin 3
20 Fin 3
21
21
22When checking argument prf to function Data.Fin.fromInteger:
22When checking argument prf to function Data.Fin.fromInteger:
23− When using n as a literal for a Fin (fromIntegerNat 3)
23+ When using n as a literal for a Fin 3
24− Could not show that n is less than fromIntegerNat 3 because n is
24+ Could not show that n is less than 3 because n is a bound
25− a bound variable instead of a constant Integer
25+ variable instead of a constant Integer
26error005.idr:28:1:When checking right hand side of x with expected type
26error005.idr:28:1:When checking right hand side of x with expected type
27 Fin 4
27 Fin 4
28
28
29When checking argument prf to function Data.Fin.fromInteger:
29When checking argument prf to function Data.Fin.fromInteger:
30− When using 5 as a literal for a Fin (fromIntegerNat 4)
30+ When using 5 as a literal for a Fin 4
31− 5 is not strictly less than fromIntegerNat 4
31+ 5 is not strictly less than 4