Normalise type when introducing lambda
We need this to get the argument type, otherwise we have to do some
needless work, also it stops scoped implicits from working properly if
we don't get the type accurately.
Fixes #3027
commitcba27c8bfab01a9e6d01ce2414954f88eadf9268
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateFri 25 Mar 2016, 20:52 (11 years ago)
parentc47296a
src/Idris/Core/Elaborate.hs+3−1
@@ -732,7 +732,9 @@ apply_elab n args =
732732checkPiGoal :: Name -> Elab' aux ()
733733checkPiGoal n
734734 = do g <- goal
735− case g of
735+ ctxt <- get_context
736+ env <- get_env
737+ case (normalise ctxt env g) of
736738 Bind _ (Pi _ _ _) _ -> return ()
737739 _ -> do a <- getNameFrom (sMN 0 "__pargTy")
738740 b <- getNameFrom (sMN 0 "__pretTy")
test/basic012/basic012a.idrnew file+10
@@ -0,0 +1,10 @@
1+Symmetric : {c : Type} -> (c -> c -> Type) -> Type
2+Symmetric {c} rel = {a : c} -> {b : c} -> rel a b -> rel b a
3+
4+record Symmetry (t : Type) (rel : t -> t -> Type) where
5+ constructor MkSymmetry
6+ is_symmetric : Symmetric {c=t} rel
7+
8+symmetry : {ty : Type} -> Symmetry ty (=)
9+symmetry = MkSymmetry sym
10+
test/basic012/run+1
@@ -1,4 +1,5 @@
11#!/usr/bin/env bash
22${IDRIS:-idris} $@ basic012.idr -o basic012
33./basic012
4+${IDRIS:-idris} $@ basic012a.idr --check
45rm -f basic012 *.ibc