git.iko.soy/Idris-dev
on master help sign in
Better typecase check

Only allow matching on polymorphic arguments if they have been refined to something concrete due to some other argument by the time they're elaborated.

commit40f6534cf00b024ec804d71af4c0e9f1bf2a309d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 22 Dec 2014, 11:22 (12 years ago) parenta2ab10c
6 files changed+35−20
compare with master
unifiedsplit
src/Idris/Delaborate.hs+1−1 src/Idris/ElabTerm.hs+16−7 test/reg010/expected+1−1 test/reg034/expected+2−2 test/reg055/expected+7−4 test/reg055/reg055a.idr+8−5
src/Idris/Delaborate.hs+1−1
@@ -263,7 +263,7 @@ pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
263263pprintErr' i (WithFnType ty) =
264264 text "Can't match on a function: type is" <+> annTm ty (pprintTerm i (delab i ty))
265265pprintErr' 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))
267267pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))
268268pprintErr' i UniverseError = text "Universe inconsistency"
269269pprintErr' i (UniqueError NullType n)
src/Idris/ElabTerm.hs+16−7
@@ -144,8 +144,8 @@ buildTC ist info emode opts fn tm
144144 where pattern = emode == ELHS
145145
146146-- 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
148−-- return type, then no, otherwise yes.
147+-- matched on. If they're polymorphic, no, unless the type has beed made
148+-- concrete by the time we get around to elaborating the argument.
149149getUnmatchable :: Context -> Name -> [Bool]
150150getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
151151 = case lookupTyExact n ctxt of
@@ -159,10 +159,7 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
159159 checkArgs env' (intersect env (refsIn t) : ns)
160160 (instantiate (P Bound n t) sc)
161161 checkArgs env ns t
162− = map (anyMissing (intersect env (refsIn t))) (reverse ns)
163−
164− anyMissing tns [] = False
165− anyMissing tns (x : xs) = not (x `elem` tns) || anyMissing tns xs
162+ = map (not . null) (reverse ns)
166163
167164getUnmatchable ctxt n = []
168165
@@ -175,6 +172,16 @@ data ElabCtxt = ElabCtxt { e_inarg :: Bool,
175172
176173initElabCtxt = ElabCtxt False False False False False
177174
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+
178185-- Returns the set of declarations we need to add to complete the definition
179186-- (most likely case blocks to elaborate)
180187
@@ -1098,9 +1105,11 @@ elab ist info emode opts fn tm
10981105 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
10991106 do focus holeName;
11001107 g <- goal
1108+ -- Can't pattern match on polymorphic goals
1109+ poly <- goal_polymorphic
11011110 ulog <- getUnifyLog
11021111 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
11041113 return failed
11051114 done_elaborating_arg f argName
11061115 elabArgs ist ina failed fc r f ns force args
test/reg010/expected+1−1
@@ -1,2 +1,2 @@
11reg010.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 @@
11reg034.idr:6:5:When elaborating left hand side of bar:
2−Can't match on bar xs xs Refl
2+Can't match on bar xs xs Refl
33reg034.idr:9:5:When elaborating left hand side of foo:
4−Can't match on foo f x x Refl
4+Can't match on foo f x x Refl
test/reg055/expected+7−4
@@ -1,6 +1,9 @@
11reg055.idr:5:3:When elaborating left hand side of g:
2−Can't match on g (f 0)
2+Can't match on g (f 0)
33reg055.idr:8:3:When elaborating left hand side of h:
4−Can't match on h x x
5−reg055a.idr:10:7:When elaborating left hand side of Foo.apply:
6−Can't match on apply (\x => \y => x) a
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 Foo.CAny:
7+ Attempting concrete match on polymorphic argument: Nothing
8+reg055a.idr:13:7:When elaborating left hand side of Foo.apply:
9+Can't match on apply (\x => \y => x) a
test/reg055/reg055a.idr+8−5
@@ -1,10 +1,13 @@
11module Foo
22
3−-- data CrappySet : (a : Type) -> Ord a -> Type where
4−-- Empty : (inst : Ord a) -> CrappySet a inst
5−-- Item : (inst : Ord a) -> a -> CrappySet a inst -> CrappySet a inst
6−--
7−-- empty : (inst : Ord a) => CrappySet a inst
3+data Cheat : Type -> Type where
4+ CAny : a -> Cheat a
5+ CInt : Cheat Int
6+
7+foo : Cheat a -> Int
8+foo (CAny Nothing) = 42
9+foo (CAny (Just x)) = 43
10+foo CInt = 0
811
912apply : (a -> a -> b) -> a -> a
1013apply (\x => \y => x) a = a