40f6534 · Idris-dev · git.iko.soy

src/Idris/Delaborate.hs+1−1

compare with master

unifiedsplit

@@ -263,7 +263,7 @@ pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

263pprintErr' i (WithFnType ty) =

264 text "Can't match on a function: type is" <+> annTm ty (pprintTerm i (delab i ty))

265pprintErr' i (CantMatch t) =

266− text "Can't match on " <+> annTm t (pprintTerm i (delab i t))

266+ text "Can't match on" <+> annTm t (pprintTerm i (delab i t))

267pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

268pprintErr' i UniverseError = text "Universe inconsistency"

269pprintErr' i (UniqueError NullType n)

src/Idris/ElabTerm.hs+16−7

@@ -144,8 +144,8 @@ buildTC ist info emode opts fn tm

144 where pattern = emode == ELHS

145

146-- return whether arguments of the given constructor name can be

147−-- matched on. If they're polymorphic and the type doesn't appear in the

147+-- matched on. If they're polymorphic, no, unless the type has beed made

148−-- return type, then no, otherwise yes.

148+-- concrete by the time we get around to elaborating the argument.

149getUnmatchable :: Context -> Name -> [Bool]

150getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon

151 = case lookupTyExact n ctxt of

@@ -159,10 +159,7 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon

159 checkArgs env' (intersect env (refsIn t) : ns)

160 (instantiate (P Bound n t) sc)

161 checkArgs env ns t

162− = map (anyMissing (intersect env (refsIn t))) (reverse ns)

162+ = map (not . null) (reverse ns)

163−

164− anyMissing tns [] = False

165− anyMissing tns (x : xs) = not (x `elem` tns) || anyMissing tns xs

166

163

167getUnmatchable ctxt n = []

164getUnmatchable ctxt n = []

168

165

@@ -175,6 +172,16 @@ data ElabCtxt = ElabCtxt { e_inarg :: Bool,

175

172

176initElabCtxt = ElabCtxt False False False False False

173initElabCtxt = ElabCtxt False False False False False

177

174

175+goal_polymorphic :: ElabD Bool

176+goal_polymorphic =

177+ do ty <- goal

178+ case ty of

179+ P _ n _ -> do env <- get_env

180+ case lookup n env of

181+ Nothing -> return False

182+ _ -> return True

183+ _ -> return False

184+

178-- Returns the set of declarations we need to add to complete the definition

185-- Returns the set of declarations we need to add to complete the definition

179-- (most likely case blocks to elaborate)

186-- (most likely case blocks to elaborate)

180

187

@@ -1098,9 +1105,11 @@ elab ist info emode opts fn tm

1098 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

1105 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

1099 do focus holeName;

1106 do focus holeName;

1100 g <- goal

1107 g <- goal

1108+ -- Can't pattern match on polymorphic goals

1109+ poly <- goal_polymorphic

1101 ulog <- getUnifyLog

1110 ulog <- getUnifyLog

1102 traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $

1111 traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $

1103− elab (ina { e_nomatching = unm }) (Just fc) t

1112+ elab (ina { e_nomatching = unm && poly }) (Just fc) t

1104 return failed

1113 return failed

1105 done_elaborating_arg f argName

1114 done_elaborating_arg f argName

1106 elabArgs ist ina failed fc r f ns force args

1115 elabArgs ist ina failed fc r f ns force args

test/reg010/expected+1−1

@@ -1,2 +1,2 @@

1reg010.idr:5:15:When elaborating left hand side of with block in usubst.unsafeSubst:

2−Can't match on with block in usubst.unsafeSubst warg a P x x px

2+Can't match on with block in usubst.unsafeSubst warg a P x x px

test/reg034/expected+2−2

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

1reg034.idr:6:5:When elaborating left hand side of bar:

2−Can't match on bar xs xs [91mRefl[0m

2+Can't match on bar xs xs [91mRefl[0m

3reg034.idr:9:5:When elaborating left hand side of foo:

4−Can't match on foo f x x [91mRefl[0m

4+Can't match on foo f x x [91mRefl[0m

test/reg055/expected+7−4

@@ -1,6 +1,9 @@

1reg055.idr:5:3:When elaborating left hand side of g:

2−Can't match on g ([92mf[0m [91m0[0m)

2+Can't match on g ([92mf[0m [91m0[0m)

3reg055.idr:8:3:When elaborating left hand side of h:

4−Can't match on h x x

4+Can't match on h x x

5+reg055a.idr:8:5:When elaborating left hand side of foo:

6+When elaborating an application of constructor [91mFoo.CAny[0m:

7+ Attempting concrete match on polymorphic argument: Nothing

5−reg055a.idr:10:7:When elaborating left hand side of Foo.apply:

8+reg055a.idr:13:7:When elaborating left hand side of Foo.apply:

6−Can't match on apply (\[95mx[0m => \[95my[0m => [95mx[0m) a

9+Can't match on apply (\[95mx[0m => \[95my[0m => [95mx[0m) a

test/reg055/reg055a.idr+8−5

@@ -1,10 +1,13 @@

1module Foo

2

3−-- data CrappySet : (a : Type) -> Ord a -> Type where

3+data Cheat : Type -> Type where

4−-- Empty : (inst : Ord a) -> CrappySet a inst

4+ CAny : a -> Cheat a

5−-- Item : (inst : Ord a) -> a -> CrappySet a inst -> CrappySet a inst

5+ CInt : Cheat Int

6−--

6+

7−-- empty : (inst : Ord a) => CrappySet a inst

7+foo : Cheat a -> Int

8+foo (CAny Nothing) = 42

9+foo (CAny (Just x)) = 43

10+foo CInt = 0

8

11

9apply : (a -> a -> b) -> a -> a

12apply : (a -> a -> b) -> a -> a

10apply (\x => \y => x) a = a

13apply (\x => \y => x) a = a