Fix bug in 'forget' for well-typed terms
Meant that sometimes if names were shadowed, the wrong ones were picked
up when rechecking, so a term which should have been well-typed was not.
Fixes #714
commitd711327076af734f9d50bd1268b9ebb07e059c2e
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSat 18 Jan 2014, 17:38 (13 years ago)
parent1c51b01
src/Idris/Core/TT.hs+3−2
@@ -863,8 +863,9 @@ forget tm = fe [] tm
863863 where
864864 fe env (P _ n _) = Var n
865865 fe env (V i) = Var (env !! i)
866− fe env (Bind n b sc) = RBind n (fmap (fe env) b)
867− (fe (n:env) sc)
866+ fe env (Bind n b sc) = let n' = uniqueName n env in
867+ RBind n' (fmap (fe env) b)
868+ (fe (n':env) sc)
868869 fe env (App f a) = RApp (fe env f) (fe env a)
869870 fe env (Constant c)
870871 = RConstant c
src/Idris/ElabDecls.hs+1
@@ -1339,6 +1339,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
13391339
13401340 ctxt <- getContext
13411341 logLvl 5 $ "Rechecking"
1342+ logLvl 6 $ " ==> " ++ show (forget rhs')
13421343 (crhs, crhsty) <- recheckC fc [] rhs'
13431344 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
13441345 case converts ctxt [] clhsty crhsty of
test/reg030/expectednew file
No changes to the content.
test/reg030/reg030.idrnew file+15
@@ -0,0 +1,15 @@
1+import Control.Isomorphism
2+
3+class Set univ where
4+ member : univ -> univ -> Type
5+
6+isSubsetOf : Set univ => univ -> univ -> Type
7+isSubsetOf {univ} a b = (c : univ) -> (member c a) -> (member c b)
8+
9+class Set univ => HasPower univ where
10+ Powerset : (a : univ) ->
11+ Exists univ (\Pa => (c : univ) ->
12+ (isSubsetOf c a) -> member c Pa)
13+
14+powerset : HasPower univ => univ -> univ
15+powerset {univ} a = getWitness (Powerset a)
test/reg030/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ reg030.idr --check
3+rm -f *.ibc