ad13438 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Check linear types in binders are valid

We need to check that a datatype with linear constructors is valid every time we encounter one at a binder, otherwise we might share by accident. This patch adds the check to the typechecker, rather than as a check in the elaborator.

commitad1343827cb052d23196494cd24659d2a38c220a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 20 Dec 2016, 21:09 (10 years ago) parent89dd6ae

5 files changed+40−21

compare with master

unifiedsplit

src/Idris/Core/Evaluate.hs+28−1 src/Idris/Core/Typecheck.hs+5 src/Idris/Elab/Type.hs+1−1 src/Idris/Elab/Utils.hs−19 src/Idris/Error.hs+6

src/Idris/Core/Evaluate.hs+28−1

@@ -27,7 +27,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

2727 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,

2828 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,

2929 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

30− isUniverse) where

30+ isUniverse, linearCheck, linearCheckArg) where

3131

3232import Idris.Core.CaseTree

3333import Idris.Core.TT

@@ -1174,6 +1174,33 @@ lookupInjectiveExact :: Name -> Context -> Maybe Injectivity

11741174lookupInjectiveExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)

11751175 where mkt (d, _, inj, a, t, m) = inj

11761176

1177+-- Assume type is at least in whnfArgs form

1178+linearCheck :: Context -> Type -> TC ()

1179+linearCheck ctxt t = checkArgs t

1180+ where

1181+ checkArgs (Bind n (Pi RigW _ ty _) sc)

1182+ = do linearCheckArg ctxt ty

1183+ checkArgs (substV (P Bound n Erased) sc)

1184+ checkArgs (Bind n (Pi _ _ _ _) sc)

1185+ = checkArgs (substV (P Bound n Erased) sc)

1186+ checkArgs _ = return ()

1187+

1188+linearCheckArg :: Context -> Type -> TC ()

1189+linearCheckArg ctxt ty = mapM_ checkNameOK (allTTNames ty)

1190+ where

1191+ checkNameOK f

1192+ = case lookupRigCountExact f ctxt of

1193+ Just Rig1 ->

1194+ tfail $ Msg $ show f ++ " can only appear in a linear binding"

1195+ _ -> return ()

1196+

1197+ checkArgs (Bind n (Pi RigW _ ty _) sc)

1198+ = do mapM_ checkNameOK (allTTNames ty)

1199+ checkArgs (substV (P Bound n Erased) sc)

1200+ checkArgs (Bind n (Pi _ _ _ _) sc)

1201+ = checkArgs (substV (P Bound n Erased) sc)

1202+ checkArgs _ = return ()

1203+

11771204-- Check if a name is reducible in the type checker. Partial definitions

11781205-- are not reducible (so treated as a constant)

11791206tcReducible :: Name -> Context -> Bool

src/Idris/Core/Typecheck.hs+5

@@ -12,6 +12,7 @@ Maintainer : The Idris Community.

1212module Idris.Core.Typecheck where

1313

1414import Idris.Core.Evaluate

15+import Idris.Core.WHNF

1516import Idris.Core.TT

1617

1718import Control.Monad.State

@@ -197,6 +198,8 @@ check' holes tcns ctxt env top

197198 constType _ = TType (UVal 0)

198199 chk rigc u lvl env (RBind n (Pi rig i s k) t)

199200 = do (sv, st, sns) <- chk Rig0 u Nothing (envZero env) s

201+ when (rig == RigW) $

202+ lift $ linearCheckArg ctxt (normalise ctxt env sv)

200203 (v, cs) <- get

201204 (kv, kt, _) <- chk Rig0 u Nothing (envZero env) k -- no need to validate these constraints, they are independent

202205 put (v+1, cs)

@@ -242,6 +245,8 @@ check' holes tcns ctxt env top

242245 chk rigc u lvl env (RBind n b sc)

243246 = do (b', bt', bns) <- checkBinder b

244247 (scv, sct, scns) <- chk rigc (smaller bt' u) Nothing ((n, getCount b, b'):env) sc

248+ when (getCount b == RigW) $

249+ lift $ linearCheckArg ctxt (normalise ctxt env (binderTy b'))

245250 checkUsageOK (getCount b) scns

246251 discharge n b' bt' (pToV n scv) (pToV n sct) (bns ++ scns)

247252 where getCount (Pi rig _ _ _) = rigMult rigc rig

src/Idris/Elab/Type.hs+1−1

@@ -136,7 +136,7 @@ buildType info syn fc opts n ty' = do

136136

137137 -- If we use any types with linear constructor arguments, we'd better

138138 -- make sure they are use-once

139− linearCheck fc (whnfArgs ctxt [] cty)

139+ tcliftAt fc $ linearCheck ctxt (whnfArgs ctxt [] cty)

140140

141141 return (cty, ckind, ty, inacc)

142142 where

src/Idris/Elab/Utils.hs−19

@@ -598,25 +598,6 @@ setLinear ns (Bind n b@(PVar r t) sc)

598598 | otherwise = Bind n b (setLinear ns sc)

599599setLinear ns tm = tm

600600

601−-- Assume type is at least in whnfArgs form

602−linearCheck :: FC -> Type -> Idris ()

603−linearCheck fc t = do ist <- getIState

604− checkArgs ist t

605− where

606− checkNameOK ist f

607− = case lookupRigCountExact f (tt_ctxt ist) of

608− Just Rig1 ->

609− ierror $ At fc $

610− Msg $ show f ++ " can only appear in a linear binding"

611− _ -> return ()

612−

613− checkArgs ist (Bind n (Pi RigW _ ty _) sc)

614− = do mapM_ (checkNameOK ist) (allTTNames ty)

615− checkArgs ist (substV (P Bound n Erased) sc)

616− checkArgs ist (Bind n (Pi _ _ _ _) sc)

617− = checkArgs ist (substV (P Bound n Erased) sc)

618− checkArgs ist _ = return ()

619−

620601linearArg :: Type -> Bool

621602linearArg (Bind n (Pi Rig1 _ _ _) sc) = True

622603linearArg (Bind n (Pi _ _ _ _) sc) = linearArg sc

src/Idris/Error.hs+6

@@ -79,6 +79,12 @@ tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err

7979tclift (Error err@(UniverseError fc _ _ _ _)) = do setErrSpan fc; throwError err

8080tclift (Error err) = throwError err

8181

82+tcliftAt :: FC -> TC a -> Idris a

83+tcliftAt fc (OK v) = return v

84+tcliftAt fc (Error err@(At _ e)) = do setErrSpan fc; throwError err

85+tcliftAt fc (Error err@(UniverseError _ _ _ _ _)) = do setErrSpan fc; throwError err

86+tcliftAt fc (Error err) = do setErrSpan fc; throwError (At fc err)

87+

8288tctry :: TC a -> TC a -> Idris a

8389tctry tc1 tc2

8490 = case tc1 of