6f30060 · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -304,6 +304,9 @@ Extra-source-files:

304 test/reg061/run

305 test/reg061/*.idr

306 test/reg061/expected

307+ test/reg062/run

308+ test/reg062/*.idr

309+ test/reg062/expected

307

310

308 test/basic001/run

311 test/basic001/run

309 test/basic001/*.idr

312 test/basic001/*.idr

src/Idris/Elab/Utils.hs+12−10

@@ -186,27 +186,29 @@ getFixedInType i _ _ _ = []

186getFlexInType i env ps (Bind n (Pi _ t _) sc)

187 = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++

188 getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)

189+

189getFlexInType i env ps tm@(App _ f a)

190getFlexInType i env ps tm@(App _ f a)

190− | (P _ tn _, args) <- unApply tm

191+ | (P nt tn _, args) <- unApply tm, nt /= Bound

191 = case lookupCtxt tn (idris_datatypes i) of

192 = case lookupCtxt tn (idris_datatypes i) of

192 [t] -> nub $ paramNames args env [x | x <- [0..length args],

193 [t] -> nub $ paramNames args env [x | x <- [0..length args],

193 not (x `elem` param_pos t)]

194 not (x `elem` param_pos t)]

194 ++ getFlexInType i env ps f ++

195 ++ getFlexInType i env ps f ++

195 getFlexInType i env ps a

196 getFlexInType i env ps a

196− [] -> let ppos = case lookupCtxt tn (idris_fninfo i) of

197+ [] -> let ppos = case lookupCtxtName tn (idris_fninfo i) of

197− [fi] -> fn_params fi

198+ [fi] -> fn_params (snd fi)

198− [] -> [] in

199+ [] -> []

200+ xs -> error ("Too much function info: " ++ show xs)

199− nub $ paramNames args env [x | x <- [0..length args],

201+ in nub $ paramNames args env [x | x <- [0..length args],

200− not (x `elem` ppos)]

202+ not (x `elem` ppos)]

201− ++ getFlexInType i env ps f ++

203+ ++ getFlexInType i env ps f ++

202− getFlexInType i env ps a

204+ getFlexInType i env ps a

203 | otherwise = nub $ getFlexInType i env ps f ++

205 | otherwise = nub $ getFlexInType i env ps f ++

204 getFlexInType i env ps a

206 getFlexInType i env ps a

205getFlexInType i _ _ _ = []

207getFlexInType i _ _ _ = []

206

208

207−-- Treat a name as a parameter if it appears in parameter positions in

209+-- | Treat a name as a parameter if it appears in parameter positions in

208-- types, and never in a non-parameter position in a (non-param) argument type.

210-- types, and never in a non-parameter position in a (non-param) argument type.

209−

211+getParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]

210getParamsInType i env ps t = let fix = getFixedInType i env ps t

212getParamsInType i env ps t = let fix = getFixedInType i env ps t

211 flex = getFlexInType i env fix t in

213 flex = getFlexInType i env fix t in

212 [x | x <- fix, not (x `elem` flex)]

214 [x | x <- fix, not (x `elem` flex)]

test/reg062/expectednew file

No changes to the content.

test/reg062/reg062.idrnew file+13

@@ -0,0 +1,13 @@

1+module MinCrash

2+

3+-- Test that #2130 stays fixed. It's important that the first argument

4+-- to revInduction be called `pred` here, because the bug was

5+-- triggered by looking up a bound variable in the global context and

6+-- getting an ambiguous result in a context where fully-qualified

7+-- names were expected.

8+

9+revInduction : (P : List a -> Type) -> P [] -> ((xs : List a) -> (x : a) -> P xs -> P (xs ++ [x]))

10+ -> (ys : List a) -> P ys

11+revInduction pred base ind ys with (reverse ys)

12+ revInduction pred base ind _ | revys =

13+ ?revInduction_rhs

test/reg062/reg062.lidrnew file+41

@@ -0,0 +1,41 @@

1+

2+This is a test to make sure that #2130 doesn't re-break.

3+

4+> import Data.Vect

5+> import Data.Fin

6+

7+> %default total

8+

9+> idSuccPreservesLTE : (m : Nat) -> (n : Nat) -> m `LTE` n -> m `LTE` (S n)

10+> idSuccPreservesLTE Z n prf = LTEZero

11+> idSuccPreservesLTE (S m) Z prf = absurd prf

12+> idSuccPreservesLTE (S m) (S n) prf = LTESucc (idSuccPreservesLTE m n (fromLteSucc prf))

13+

14+> ltZS : (m : Nat) -> LT Z (S m)

15+> ltZS Z = LTESucc LTEZero

16+> ltZS (S m) = idSuccPreservesLTE (S Z) (S m) (ltZS m)

17+

18+> record Preorder : {T : Type} -> (T -> T -> Type) -> Type where

19+> MkPreorder : {T : Type} ->

20+> (R : T -> T -> Type) ->

21+> (reflexive : (x : T) -> R x x) ->

22+> (transitive : (x : T) -> (y : T) -> (z : T) -> R x y -> R y z -> R x z) ->

23+> Preorder R

24+

25+> record TotalPreorder : {T : Type} -> (T -> T -> Type) -> Type where

26+> MkTotalPreorder : {T : Type} ->

27+> (R : T -> T -> Type) ->

28+> (reflexive : (x : T) -> R x x) ->

29+> (transitive : (x : T) -> (y : T) -> (z : T) -> R x y -> R y z -> R x z) ->

30+> (either : (x : T) -> (y : T) -> Either (R x y) (R y x)) ->

31+> TotalPreorder R

32+

33+> argmaxMax : {A : Type} -> {R : A -> A -> Type} -> TotalPreorder {T = A} R ->

34+> Vect n A -> LT Z n -> (Fin n, A)

35+> argmaxMax {n = Z} tp Nil p = absurd p

36+> argmaxMax {n = S Z} tp (a :: Nil) _ = (FZ, a)

37+> argmaxMax {A} {R} {n = S (S m)} (MkTotalPreorder R r t e) (a' :: (a'' :: as)) _

38+> with (argmaxMax (MkTotalPreorder {T = A} R r t e) (a'' :: as) (ltZS m))

39+> | (k, max) with (e a' max)

40+> | (Left _) = (FS k, max)

41+> | (Right _) = (FZ, a')

test/reg062/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ reg062.idr --check --nocolour

3+idris $@ reg062.lidr --check --nocolour

4+rm -f *.ibc