d711327 · Idris-dev · git.iko.soy

src/Idris/Core/TT.hs+3−2

compare with master

unifiedsplit

@@ -863,8 +863,9 @@ forget tm = fe [] tm

863 where

864 fe env (P _ n _) = Var n

865 fe env (V i) = Var (env !! i)

866+ fe env (Bind n b sc) = let n' = uniqueName n env in

866− fe env (Bind n b sc) = RBind n (fmap (fe env) b)

867+ RBind n' (fmap (fe env) b)

867− (fe (n:env) sc)

868+ (fe (n':env) sc)

868 fe env (App f a) = RApp (fe env f) (fe env a)

869 fe env (App f a) = RApp (fe env f) (fe env a)

869 fe env (Constant c)

870 fe env (Constant c)

870 = RConstant c

871 = RConstant c

src/Idris/ElabDecls.hs+1

@@ -1339,6 +1339,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1339

1340 ctxt <- getContext

1341 logLvl 5 $ "Rechecking"

1342+ logLvl 6 $ " ==> " ++ show (forget rhs')

1342 (crhs, crhsty) <- recheckC fc [] rhs'

1343 (crhs, crhsty) <- recheckC fc [] rhs'

1343 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

1344 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

1344 case converts ctxt [] clhsty crhsty of

1345 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