5521f95 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Don't allow matching on functions without justification

Otherwise we have patterns which type check, and which are considered total, but which can't be properly check at run-time. Fixes #138

commit5521f9516d58a62a033d9d9699d492765d4a4631 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 22 Nov 2013, 14:34 (13 years ago) parent543cd7e

2 files changed+21−1

unifiedsplit

src/Idris/AbsSyntax.hs+19

@@ -1282,6 +1282,25 @@ stripLinear i tm = evalState (sl tm) [] where

12821282 return $ PTacImplicit p l n sc t' d

12831283 sl x = return x

12841284

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+

12851304mkPApp fc a f [] = f

12861305mkPApp fc a f as = let rest = drop a as in

12871306 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)

930930 [t] -> t

931931 _ -> []

932932 let params = getParamsInType i [] fn_is fn_ty

933− let lhs = addImplPat i (propagateParams params (stripLinear i lhs_in))

933+ let lhs = stripUnmatchable i $

934+ addImplPat i (propagateParams params (stripLinear i lhs_in))

934935 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)

935936 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

936937