git.iko.soy/Idris-dev
on master help sign in
Don't allow matching on functions without justification
5521f95Edwin Brady
src/Idris/AbsSyntax.hs+19
compare with master
unifiedsplit
@@ -1282,6 +1282,25 @@ stripLinear i tm = evalState (sl tm) [] where
1282 return $ PTacImplicit p l n sc t' d
1282 return $ PTacImplicit p l n sc t' d
1283 sl x = return x
1283 sl x = return x
1284
1284
1285+-- Remove functions which aren't applied to anything, which must then
1286+-- be resolved by unification. Assume names resolved and alternatives
1287+-- filled in (so no ambiguity).
1288+
1289+stripUnmatchable :: IState -> PTerm -> PTerm
1290+stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1291+ su :: PTerm -> PTerm
1292+ su (PRef fc f)
1293+ | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1294+ = Placeholder
1295+ su (PApp fc fn args)
1296+ = PApp fc fn (fmap (fmap su) args)
1297+ su (PAlternative b alts)
1298+ = PAlternative b (filter (/= Placeholder) (map su alts))
1299+ su (PPair fc l r) = PPair fc (su l) (su r)
1300+ su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)
1301+ su t = t
1302+stripUnmatchable i tm = tm
1303+
1285mkPApp fc a f [] = f
1304mkPApp fc a f [] = f
1286mkPApp fc a f as = let rest = drop a as in
1305mkPApp fc a f as = let rest = drop a as in
1287 appRest fc (PApp fc f (take a as)) rest
1306 appRest fc (PApp fc f (take a as)) rest
src/Idris/ElabDecls.hs+2−1
@@ -930,7 +930,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
930 [t] -> t
930 [t] -> t
931 _ -> []
931 _ -> []
932 let params = getParamsInType i [] fn_is fn_ty
932 let params = getParamsInType i [] fn_is fn_ty
933+ let lhs = stripUnmatchable i $
933− let lhs = addImplPat i (propagateParams params (stripLinear i lhs_in))
934+ addImplPat i (propagateParams params (stripLinear i lhs_in))
934 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)
935 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)
935 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
936 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
936
937