53ffd07 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Injectivity assumptions

Parameters should only be assumed to be injective if they also happen to be type class parameters, otherwise some things will type check which otherwise shouldn't.

commit53ffd071d58d43c85c60e4e301c4615f0ba69abb authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 1 Sep 2015, 11:54 (11 years ago) parentcf47310

2 files changed+24−2

compare with master

unifiedsplit

src/Idris/Elab/Clause.hs+5−2 src/Idris/Elab/Utils.hs+19

src/Idris/Elab/Clause.hs+5−2

@@ -543,7 +543,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

543543 let fn_is = case lookupCtxt fname (idris_implicits i) of

544544 [t] -> t

545545 _ -> []

546− let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)

546+ let norm_ty = normalise ctxt [] fn_ty

547+ let params = getParamsInType i [] fn_is norm_ty

548+ let tcparams = getTCParamsInType i [] fn_is norm_ty

549+

547550 let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $

548551 propagateParams i params fn_ty (addImplPat i lhs_in)

549552-- let lhs = mkLHSapp $

@@ -634,7 +637,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

634637 (do pbinds ist lhs_tm

635638 -- proof search can use explicitly written names

636639 mapM_ addPSname (allNamesIn lhs_in)

637− mapM_ setinj (nub (params ++ inj))

640+ mapM_ setinj (nub (tcparams ++ inj))

638641 setNextName

639642 (ElabResult _ _ is ctxt' newDecls highlights) <-

640643 errAt "right hand side of " fname

src/Idris/Elab/Utils.hs+19

@@ -16,6 +16,7 @@ import Control.Applicative hiding (Const)

1616import Control.Monad.State

1717import Control.Monad

1818import Data.List

19+import Data.Maybe

1920import qualified Data.Traversable as Traversable

2021

2122import Debug.Trace

@@ -211,6 +212,24 @@ getParamsInType i env ps t = let fix = getFixedInType i env ps t

211212 flex = getFlexInType i env fix t in

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

213214

215+getTCinj i (Bind n (Pi _ t _) sc)

216+ = getTCinj i t ++ getTCinj i (instantiate (P Bound n t) sc)

217+getTCinj i ap@(App _ f a)

218+ | (P _ n _, args) <- unApply ap,

219+ isTCName n = mapMaybe getInjName args

220+ | otherwise = []

221+ where

222+ isTCName n = case lookupCtxtExact n (idris_classes i) of

223+ Just _ -> True

224+ _ -> False

225+ getInjName t | (P _ x _, _) <- unApply t = Just x

226+ | otherwise = Nothing

227+getTCinj _ _ = []

228+

229+getTCParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]

230+getTCParamsInType i env ps t = let params = getParamsInType i env ps t

231+ tcs = nub $ getTCinj i t in

232+ filter (flip elem tcs) params

214233paramNames args env [] = []

215234paramNames args env (p : ps)

216235 | length args > p = case args!!p of