7e7368d · Idris-dev · git.iko.soy

libs/base/Language/Reflection.idr+7−6

compare with master

unifiedsplit

@@ -92,7 +92,7 @@ data NameType = Bound

92||| Types annotations for bound variables in different

93||| binding contexts

94data Binder a = Lam a

95− | Pi a

95+ | Pi a a

96 | Let a a

97 | NLet a a

98 | Hole a

@@ -104,7 +104,7 @@ data Binder a = Lam a

104

105instance Functor Binder where

106 map f (Lam x) = Lam (f x)

107− map f (Pi x) = Pi (f x)

107+ map f (Pi x k) = Pi (f x) (f k)

108 map f (Let x y) = Let (f x) (f y)

109 map f (NLet x y) = NLet (f x) (f y)

110 map f (Hole x) = Hole (f x)

@@ -115,7 +115,7 @@ instance Functor Binder where

115

116instance Foldable Binder where

117 foldr f z (Lam x) = f x z

118− foldr f z (Pi x) = f x z

118+ foldr f z (Pi x k) = f x (f k z)

119 foldr f z (Let x y) = f x (f y z)

120 foldr f z (NLet x y) = f x (f y z)

121 foldr f z (Hole x) = f x z

@@ -126,7 +126,7 @@ instance Foldable Binder where

126

127instance Traversable Binder where

128 traverse f (Lam x) = [| Lam (f x) |]

129− traverse f (Pi x) = [| Pi (f x) |]

129+ traverse f (Pi x k) = [| Pi (f x) (f k) |]

130 traverse f (Let x y) = [| Let (f x) (f y) |]

131 traverse f (NLet x y) = [| NLet (f x) (f y) |]

132 traverse f (Hole x) = [| Hole (f x) |]

@@ -400,7 +400,8 @@ mutual

400 instance Quotable (Binder TT) where

401 quotedTy = `(Binder TT)

402 quote (Lam x) = `(Lam {a=TT} ~(assert_total (quote x)))

403− quote (Pi x) = `(Pi {a=TT} ~(assert_total (quote x)))

403+ quote (Pi x k) = `(Pi {a=TT} ~(assert_total (quote x))

404+ ~(assert_total (quote k)))

404 quote (Let x y) = `(Let {a=TT} ~(assert_total (quote x))

405 quote (Let x y) = `(Let {a=TT} ~(assert_total (quote x))

405 ~(assert_total (quote y)))

406 ~(assert_total (quote y)))

406 quote (NLet x y) = `(NLet {a=TT} ~(assert_total (quote x))

407 quote (NLet x y) = `(NLet {a=TT} ~(assert_total (quote x))

@@ -431,7 +432,7 @@ mutual

431

432

432 quoteRawBinder : Binder Raw -> TT

433 quoteRawBinder : Binder Raw -> TT

433 quoteRawBinder (Lam x) = `(Lam {a=Raw} ~(quoteRaw x))

434 quoteRawBinder (Lam x) = `(Lam {a=Raw} ~(quoteRaw x))

434− quoteRawBinder (Pi x) = `(Pi {a=Raw} ~(quoteRaw x))

435+ quoteRawBinder (Pi x k) = `(Pi {a=Raw} ~(quoteRaw x) ~(quoteRaw k))

435 quoteRawBinder (Let x y) = `(Let {a=Raw} ~(quoteRaw x) ~(quoteRaw y))

436 quoteRawBinder (Let x y) = `(Let {a=Raw} ~(quoteRaw x) ~(quoteRaw y))

436 quoteRawBinder (NLet x y) = `(NLet {a=Raw} ~(quoteRaw x) ~(quoteRaw y))

437 quoteRawBinder (NLet x y) = `(NLet {a=Raw} ~(quoteRaw x) ~(quoteRaw y))

437 quoteRawBinder (Hole x) = `(Hole {a=Raw} ~(quoteRaw x))

438 quoteRawBinder (Hole x) = `(Hole {a=Raw} ~(quoteRaw x))

libs/base/Language/Reflection/Utils.idr+3−3

@@ -48,7 +48,7 @@ mkApp tm (a::as) = mkApp (App tm a) as

48

49binderTy : (Eq t) => Binder t -> t

50binderTy (Lam t) = t

51−binderTy (Pi t) = t

51+binderTy (Pi t _) = t

52binderTy (Let t1 t2) = t1

53binderTy (NLet t1 t2) = t1

54binderTy (Hole t) = t

@@ -160,7 +160,7 @@ instance Eq NameType where

160

161instance (Show a) => Show (Binder a) where

162 show (Lam t) = "(Lam " ++ show t ++ ")"

163− show (Pi t) = "(Pi " ++ show t ++ ")"

163+ show (Pi t _) = "(Pi " ++ show t ++ ")"

164 show (Let t1 t2) = "(Let " ++ show t1 ++ " " ++ show t2 ++ ")"

165 show (NLet t1 t2) = "(NLet " ++ show t1 ++ " " ++ show t2 ++ ")"

166 show (Hole t) = "(Hole " ++ show t ++ ")"

@@ -171,7 +171,7 @@ instance (Show a) => Show (Binder a) where

171

172instance (Eq a) => Eq (Binder a) where

173 (Lam t) == (Lam t') = t == t'

174− (Pi t) == (Pi t') = t == t'

174+ (Pi t k) == (Pi t' k') = t == t' && k == k'

175 (Let t1 t2) == (Let t1' t2') = t1 == t1' && t2 == t2'

176 (NLet t1 t2) == (NLet t1' t2') = t1 == t1' && t2 == t2'

177 (Hole t) == (Hole t') = t == t'

src/Idris/AbsSyntax.hs+6−6

@@ -1065,7 +1065,7 @@ addStatics n tm ptm =

1065 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }

1066 addIBC (IBCStatic n)

1067 where

1068− initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)

1068+ initStatics (Bind n (Pi ty _) sc) (PPi p _ _ s)

1069 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in

1070 if pstatic p == Static then ((n, ty) : static, dynamic)

1071 else if (not (searchArg p))

@@ -1073,7 +1073,7 @@ addStatics n tm ptm =

1073 else (static, dynamic)

1074 initStatics t pt = ([], [])

1075

1076− freeArgNames (Bind n (Pi ty) sc)

1076+ freeArgNames (Bind n (Pi ty _) sc)

1077 = nub $ freeArgNames ty

1078 freeArgNames tm = let (_, args) = unApply tm in

1079 concatMap freeNames args

@@ -1085,7 +1085,7 @@ addStatics n tm ptm =

1085 searchArg (TacImp _ _ _) = True

1086 searchArg _ = False

1087

1088− staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc

1088+ staticList sts (Bind n (Pi _ _) sc) = (n `elem` sts) : staticList sts sc

1089 staticList _ _ = []

1090

1091-- Dealing with implicit arguments

@@ -1186,7 +1186,7 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

1186 = (n, (p, t)) : collectImps sc

1187 collectImps _ = []

1188

1189− getImps (Bind n (Pi t) sc) imps

1189+ getImps (Bind n (Pi t _) sc) imps

1190 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

1191 where

1192 argInfo n (Imp opt _ _) t'

@@ -1200,7 +1200,7 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

1200 argInfo n (TacImp opt _ scr) t'

1201 = (InaccessibleArg `elem` opt,

1202 PTacImplicit 10 opt n scr t')

1203− getImps (Bind n (Pi t) sc) imps = impBind n t : getImps sc imps

1203+ getImps (Bind n (Pi t _) sc) imps = impBind n t : getImps sc imps

1204 where impBind n t = (True, PImp 1 True [] n Placeholder)

1205 getImps sc tm = []

1206

@@ -1612,7 +1612,7 @@ stripUnmatchable :: IState -> PTerm -> PTerm

1612stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1613 su :: PTerm -> PTerm

1614 su (PRef fc f)

1615− | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)

1615+ | (Bind n (Pi t _) sc :_) <- lookupTy f (tt_ctxt i)

1616 = Placeholder

1617 su (PApp fc fn args)

1618 = PApp fc fn (fmap (fmap su) args)

src/Idris/AbsSyntaxTree.hs+1−1

@@ -1050,7 +1050,7 @@ getInferTerm (App (App _ _) tm) = tm

1050getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

1051

1052getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc

1053− where toTy (Lam t) = Pi t

1053+ where toTy (Lam t) = Pi t (TType (UVar 0))

1054 toTy (PVar t) = PVTy t

1055 toTy b = b

1056getInferType (App (App _ ty) _) = ty

src/Idris/Apropos.hs+1−1

@@ -53,7 +53,7 @@ instance Apropos Def where

53

54instance Apropos (Binder (TT Name)) where

55 isApropos str (Lam ty) = str == T.pack "\\" || isApropos str ty

56− isApropos str (Pi ty) = str == T.pack "->" || isApropos str ty

56+ isApropos str (Pi ty _) = str == T.pack "->" || isApropos str ty

57 isApropos str (Let ty val) = str == T.pack "let" || isApropos str ty || isApropos str val

58 isApropos str (NLet ty val) = str == T.pack "let" || isApropos str ty || isApropos str val

59 isApropos str _ = False -- these shouldn't occur in defined libraries

src/Idris/CaseSplit.hs+1−1

@@ -176,7 +176,7 @@ argTys ist (PRef fc n)

176 = case lookupTy n (tt_ctxt ist) of

177 [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing

178 _ -> repeat Nothing

179− where tyName (Bind _ (Pi _) _) = Just (sUN "->")

179+ where tyName (Bind _ (Pi _ _) _) = Just (sUN "->")

180 tyName t | (P _ n _, _) <- unApply t = Just n

181 | otherwise = Nothing

182argTys _ _ = repeat Nothing

src/Idris/Core/Binary.hs+5−3

@@ -233,8 +233,9 @@ instance (Binary b) => Binary (Binder b) where

233 = case x of

234 Lam x1 -> do putWord8 0

235 put x1

236− Pi x1 -> do putWord8 1

236+ Pi x1 x2 -> do putWord8 1

237− put x1

237+ put x1

238+ put x2

238 Let x1 x2 -> do putWord8 2

239 Let x1 x2 -> do putWord8 2

239 put x1

240 put x1

240 put x2

241 put x2

@@ -259,7 +260,8 @@ instance (Binary b) => Binary (Binder b) where

259 0 -> do x1 <- get

260 0 -> do x1 <- get

260 return (Lam x1)

261 return (Lam x1)

261 1 -> do x1 <- get

262 1 -> do x1 <- get

263+ x2 <- get

262− return (Pi x1)

264+ return (Pi x1 x2)

263 2 -> do x1 <- get

265 2 -> do x1 <- get

264 x2 <- get

266 x2 <- get

265 return (Let x1 x2)

267 return (Let x1 x2)

src/Idris/Core/CaseTree.hs+1−1

@@ -370,7 +370,7 @@ toPat reflect tc = map $ toPat' []

370 toPat' [] (Constant VoidType) = PTyPat

371 toPat' [] (Constant x) = PConst x

372

373− toPat' [] (Bind n (Pi t) sc)

373+ toPat' [] (Bind n (Pi t _) sc)

374 | reflect && noOccurrence n sc

375 = PReflected (sUN "->") [toPat' [] t, toPat' [] sc]

376

src/Idris/Core/DeepSeq.hs+1−1

@@ -70,7 +70,7 @@ instance NFData Err where

70

71instance (NFData b) => NFData (Binder b) where

72 rnf (Lam x1) = rnf x1 `seq` ()

73− rnf (Pi x1) = rnf x1 `seq` ()

73+ rnf (Pi x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

74 rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

75 rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

76 rnf (Hole x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs+6−6

@@ -254,7 +254,7 @@ checkInjective (tm, l, r) = do ctxt <- get_context

254 isInj ctxt (App f a) = isInj ctxt f

255 isInj ctxt (Constant _) = True

256 isInj ctxt (TType _) = True

257− isInj ctxt (Bind _ (Pi _) sc) = True

257+ isInj ctxt (Bind _ (Pi _ _) sc) = True

258 isInj ctxt _ = False

259

260-- get instance argument names

@@ -454,7 +454,7 @@ prepare_apply fn imps =

454 -> [(Name, Name)] -- ^ Accumulator for produced claims

455 -> [Name] -- ^ Hypotheses

456 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.

457− mkClaims (Bind n' (Pi t_in) sc) (i : is) claims hs =

457+ mkClaims (Bind n' (Pi t_in _) sc) (i : is) claims hs =

458 do let t = rebind hs t_in

459 n <- getNameFrom (mkMN n')

460-- when (null claims) (start_unify n)

@@ -562,7 +562,7 @@ apply_elab n args =

562 priOrder _ Nothing = GT

563 priOrder (Just (x, _)) (Just (y, _)) = compare x y

564

565− doClaims (Bind n' (Pi t) sc) (i : is) claims =

565+ doClaims (Bind n' (Pi t _) sc) (i : is) claims =

566 do n <- unique_hole (mkMN n')

567 when (null claims) (start_unify n)

568 let sc' = instantiate (P Bound n t) sc

@@ -597,13 +597,13 @@ checkPiGoal :: Name -> Elab' aux ()

597checkPiGoal n

598 = do g <- goal

599 case g of

600− Bind _ (Pi _) _ -> return ()

600+ Bind _ (Pi _ _) _ -> return ()

601 _ -> do a <- getNameFrom (sMN 0 "pargTy")

602 b <- getNameFrom (sMN 0 "pretTy")

603 f <- getNameFrom (sMN 0 "pf")

604 claim a RType

605 claim b RType

606− claim f (RBind n (Pi (Var a)) (Var b))

606+ claim f (RBind n (Pi (Var a) RType) (Var b))

607 movelast a

608 movelast b

609 fill (Var f)

@@ -618,7 +618,7 @@ simple_app fun arg appstr =

618 s <- getNameFrom (sMN 0 "s")

619 claim a RType

620 claim b RType

621− claim f (RBind (sMN 0 "aX") (Pi (Var a)) (Var b))

621+ claim f (RBind (sMN 0 "aX") (Pi (Var a) RType) (Var b))

622 tm <- get_term

623 start_unify s

624 claim s (Var a)

src/Idris/Core/Evaluate.hs+14−12

@@ -239,20 +239,21 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

239 ev ntimes stk top env (V i)

240 | i < length env && i >= 0 = return $ snd (env !! i)

241 | otherwise = return $ VV i

242− ev ntimes stk top env (Bind n (Let t v) sc)

242+ ev ntimes stk top env (Bind n (Let t v) sc)

243+ | not runtime || occurrences n sc < 2

243 = do v' <- ev ntimes stk top env v --(finalise v)

244 = do v' <- ev ntimes stk top env v --(finalise v)

244 sc' <- ev ntimes stk top ((n, v') : env) sc

245 sc' <- ev ntimes stk top ((n, v') : env) sc

245 wknV (-1) sc'

246 wknV (-1) sc'

246−-- | otherwise

247+ | otherwise

247−-- = do t' <- ev ntimes stk top env t

248+ = do t' <- ev ntimes stk top env t

248−-- v' <- ev ntimes stk top env v --(finalise v)

249+ v' <- ev ntimes stk top env v --(finalise v)

249−-- -- use Tmp as a placeholder, then make it a variable reference

250+ -- use Tmp as a placeholder, then make it a variable reference

250−-- -- again when evaluation finished

251+ -- again when evaluation finished

251−-- hs <- get

252+ hs <- get

252−-- let vd = nexthole hs

253+ let vd = nexthole hs

253−-- put (hs { nexthole = vd + 1 })

254+ put (hs { nexthole = vd + 1 })

254−-- sc' <- ev ntimes stk top (VP Bound (MN vd "vlet") VErased : env) sc

255+ sc' <- ev ntimes stk top ((n, VP Bound (sMN vd "vlet") VErased) : env) sc

255−-- return $ VBLet vd n t' v' sc'

256+ return $ VBLet vd n t' v' sc'

256 ev ntimes stk top env (Bind n (NLet t v) sc)

257 ev ntimes stk top env (Bind n (NLet t v) sc)

257 = do t' <- ev ntimes stk top env (finalise t)

258 = do t' <- ev ntimes stk top env (finalise t)

258 v' <- ev ntimes stk top env (finalise v)

259 v' <- ev ntimes stk top env (finalise v)

@@ -437,7 +438,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

437 | Just v <- findDefault alts = return $ Just (amap, v)

438 | Just v <- findDefault alts = return $ Just (amap, v)

438 chooseAlt env _ (VP _ n _, args) alts amap

439 chooseAlt env _ (VP _ n _, args) alts amap

439 | Just (ns, sc) <- findFn n alts = return $ Just (updateAmap (zip ns args) amap, sc)

440 | Just (ns, sc) <- findFn n alts = return $ Just (updateAmap (zip ns args) amap, sc)

440− chooseAlt env _ (VBind _ _ (Pi s) t, []) alts amap

441+ chooseAlt env _ (VBind _ _ (Pi s k) t, []) alts amap

441 | Just (ns, sc) <- findFn (sUN "->") alts

442 | Just (ns, sc) <- findFn (sUN "->") alts

442 = do t' <- t (VV 0) -- we know it's not in scope or it's not a pattern

443 = do t' <- t (VV 0) -- we know it's not in scope or it's not a pattern

443 return $ Just (updateAmap (zip ns [s, t']) amap, sc)

444 return $ Just (updateAmap (zip ns [s, t']) amap, sc)

@@ -580,6 +581,7 @@ convEq ctxt holes topx topy = ceq [] topx topy where

580 where

581 where

581 ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

582 ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

582 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

583 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

584+ ceqB ps (Pi v t) (Pi v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

583 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')

585 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')

584 ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)

586 ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)

585 ceq ps (Constant x) (Constant y) = return (x == y)

587 ceq ps (Constant x) (Constant y) = return (x == y)

src/Idris/Core/Execute.hs+1−1

@@ -84,7 +84,7 @@ toTT (EBind n b body) = do body' <- body $ EP Bound n EErased

84 b' <- fixBinder b

85 Bind n b' <$> toTT body'

86 where fixBinder (Lam t) = Lam <$> toTT t

87− fixBinder (Pi t) = Pi <$> toTT t

87+ fixBinder (Pi t k) = Pi <$> toTT t <*> toTT k

88 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

89 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

90 fixBinder (Hole t) = Hole <$> toTT t

src/Idris/Core/ProofState.hs+11−11

@@ -396,7 +396,7 @@ defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

396 (mkApp (P Ref n ty) (map getP (reverse env'))))

397 where

398 mkTy [] t = t

399− mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)

399+ mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b) (TType (UVar 0))) (mkTy bs t)

400

401 getP (n, b) = P Bound n (binderTy b)

402

@@ -515,17 +515,17 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

515 Just name -> name

516 Nothing -> x

517 let t' = case t of

518− x@(Bind y (Pi s) _) -> x

518+ x@(Bind y (Pi s _) _) -> x

519 _ -> hnf ctxt env t

520 (tyv, tyt) <- lift $ check ctxt env ty

521-- ns <- lift $ unify ctxt env tyv t'

522 case t' of

523− Bind y (Pi s) t -> let t' = subst y (P Bound n s) t in

523+ Bind y (Pi s _) t -> let t' = subst y (P Bound n s) t in

524− do ns <- unify' ctxt env s tyv

524+ do ns <- unify' ctxt env s tyv

525− ps <- get

525+ ps <- get

526− let (uh, uns) = unified ps

526+ let (uh, uns) = unified ps

527−-- put (ps { unified = (uh, uns ++ ns) })

527+-- put (ps { unified = (uh, uns ++ ns) })

528− return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))

528+ return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))

529 _ -> lift $ tfail $ CantIntroduce t'

530introTy ty n ctxt env _ = fail "Can't introduce here."

531

@@ -535,10 +535,10 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

535 Just name -> name

536 Nothing -> x

537 let t' = case t of

538− x@(Bind y (Pi s) _) -> x

538+ x@(Bind y (Pi s _) _) -> x

539 _ -> hnf ctxt env t

540 case t' of

541− Bind y (Pi s) t -> -- trace ("in type " ++ show t') $

541+ Bind y (Pi s _) t -> -- trace ("in type " ++ show t') $

542 let t' = subst y (P Bound n s) t in

543 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

544 _ -> lift $ tfail $ CantIntroduce t'

@@ -549,7 +549,7 @@ forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

549 do (tyv, tyt) <- lift $ check ctxt env ty

550 unify' ctxt env tyt (TType (UVar 0))

551 unify' ctxt env t (TType (UVar 0))

552− return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))

552+ return $ Bind n (Pi tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))

553forall n ty ctxt env _ = fail "Can't pi bind here"

554

555patvar :: Name -> RunTactic

src/Idris/Core/TT.hs+35−17

@@ -640,7 +640,8 @@ deriving instance NFData Raw

640-- the types of bindings (and their values, if any); the attached identifiers are part

641-- of the 'Bind' constructor for the 'TT' type.

642data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}

643− | Pi { binderTy :: !b }

643+ | Pi { binderTy :: !b,

644+ binderKind :: !b }

644 {-^ A binding that occurs in a function type expression, e.g. @(x:Int) -> ...@ -}

645 {-^ A binding that occurs in a function type expression, e.g. @(x:Int) -> ...@ -}

645 | Let { binderTy :: !b,

646 | Let { binderTy :: !b,

646 binderVal :: b {-^ value for bound variable-}}

647 binderVal :: b {-^ value for bound variable-}}

@@ -663,7 +664,7 @@ deriving instance NFData Binder

663

664

664instance Sized a => Sized (Binder a) where

665instance Sized a => Sized (Binder a) where

665 size (Lam ty) = 1 + size ty

666 size (Lam ty) = 1 + size ty

666− size (Pi ty) = 1 + size ty

667+ size (Pi ty _) = 1 + size ty

667 size (Let ty val) = 1 + size ty + size val

668 size (Let ty val) = 1 + size ty + size val

668 size (NLet ty val) = 1 + size ty + size val

669 size (NLet ty val) = 1 + size ty + size val

669 size (Hole ty) = 1 + size ty

670 size (Hole ty) = 1 + size ty

@@ -677,9 +678,9 @@ fmapMB f (Let t v) = liftM2 Let (f t) (f v)

677fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)

678fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)

678fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)

679fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)

679fmapMB f (Lam t) = liftM Lam (f t)

680fmapMB f (Lam t) = liftM Lam (f t)

680−fmapMB f (Pi t) = liftM Pi (f t)

681+fmapMB f (Pi t k) = liftM2 Pi (f t) (f k)

681fmapMB f (Hole t) = liftM Hole (f t)

682fmapMB f (Hole t) = liftM Hole (f t)

682−fmapMB f (GHole i t) = liftM (GHole i) (f t)

683+fmapMB f (GHole i t) = liftM (GHole i) (f t)

683fmapMB f (PVar t) = liftM PVar (f t)

684fmapMB f (PVar t) = liftM PVar (f t)

684fmapMB f (PVTy t) = liftM PVTy (f t)

685fmapMB f (PVTy t) = liftM PVTy (f t)

685

686

@@ -844,7 +845,7 @@ isInjective (P (DCon _ _ _) _ _) = True

844isInjective (P (TCon _ _) _ _) = True

845isInjective (P (TCon _ _) _ _) = True

845isInjective (Constant _) = True

846isInjective (Constant _) = True

846isInjective (TType x) = True

847isInjective (TType x) = True

847−isInjective (Bind _ (Pi _) sc) = True

848+isInjective (Bind _ (Pi _ _) sc) = True

848isInjective (App f a) = isInjective f

849isInjective (App f a) = isInjective f

849isInjective _ = False

850isInjective _ = False

850

851

@@ -1017,6 +1018,20 @@ substTerm old new = st where

1017 st (Bind x b sc) = Bind x (fmap st b) (st sc)

1018 st (Bind x b sc) = Bind x (fmap st b) (st sc)

1018 st t = t

1019 st t = t

1019

1020

1021+-- | Return number of occurrences of V 0 or bound name i the term

1022+occurrences :: Eq n => n -> TT n -> Int

1023+occurrences n t = execState (no' 0 t) 0

1024+ where

1025+ no' i (V x) | i == x = do num <- get; put (num + 1)

1026+ no' i (P Bound x _) | n == x = do num <- get; put (num + 1)

1027+ no' i (Bind n b sc) = do noB' i b; no' (i+1) sc

1028+ where noB' i (Let t v) = do no' i t; no' i v

1029+ noB' i (Guess t v) = do no' i t; no' i v

1030+ noB' i b = no' i (binderTy b)

1031+ no' i (App f a) = do no' i f; no' i a

1032+ no' i (Proj x _) = no' i x

1033+ no' i _ = return ()

1034+

1020-- | Returns true if V 0 and bound name n do not occur in the term

1035-- | Returns true if V 0 and bound name n do not occur in the term

1021noOccurrence :: Eq n => n -> TT n -> Bool

1036noOccurrence :: Eq n => n -> TT n -> Bool

1022noOccurrence n t = no' 0 t

1037noOccurrence n t = no' 0 t

@@ -1043,7 +1058,7 @@ freeNames _ = []

1043

1058

1044-- | Return the arity of a (normalised) type

1059-- | Return the arity of a (normalised) type

1045arity :: TT n -> Int

1060arity :: TT n -> Int

1046−arity (Bind n (Pi t) sc) = 1 + arity sc

1061+arity (Bind n (Pi t _) sc) = 1 + arity sc

1047arity _ = 0

1062arity _ = 0

1048

1063

1049-- | Deconstruct an application; returns the function and a list of arguments

1064-- | Deconstruct an application; returns the function and a list of arguments

@@ -1100,13 +1115,13 @@ bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)

1100-- | Return a list of pairs of the names of the outermost 'Pi'-bound

1115-- | Return a list of pairs of the names of the outermost 'Pi'-bound

1101-- variables in the given term, together with their types.

1116-- variables in the given term, together with their types.

1102getArgTys :: TT n -> [(n, TT n)]

1117getArgTys :: TT n -> [(n, TT n)]

1103−getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc

1118+getArgTys (Bind n (Pi t _) sc) = (n, t) : getArgTys sc

1104getArgTys _ = []

1119getArgTys _ = []

1105

1120

1106getRetTy :: TT n -> TT n

1121getRetTy :: TT n -> TT n

1107getRetTy (Bind n (PVar _) sc) = getRetTy sc

1122getRetTy (Bind n (PVar _) sc) = getRetTy sc

1108getRetTy (Bind n (PVTy _) sc) = getRetTy sc

1123getRetTy (Bind n (PVTy _) sc) = getRetTy sc

1109−getRetTy (Bind n (Pi _) sc) = getRetTy sc

1124+getRetTy (Bind n (Pi _ _) sc) = getRetTy sc

1110getRetTy sc = sc

1125getRetTy sc = sc

1111

1126

1112uniqueNameFrom :: [Name] -> [Name] -> Name

1127uniqueNameFrom :: [Name] -> [Name] -> Name

@@ -1212,7 +1227,7 @@ prettyEnv env t = prettyEnv' env t False

1212 else

1227 else

1213 lbracket <+> text (show i) <+> rbracket

1228 lbracket <+> text (show i) <+> rbracket

1214 | otherwise = text "unbound" <+> text (show i) <+> text "!"

1229 | otherwise = text "unbound" <+> text (show i) <+> text "!"

1215− prettySe p env (Bind n b@(Pi t) sc) debug

1230+ prettySe p env (Bind n b@(Pi t _) sc) debug

1216 | noOccurrence n sc && not debug =

1231 | noOccurrence n sc && not debug =

1217 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug

1232 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug

1218 prettySe p env (Bind n b sc) debug =

1233 prettySe p env (Bind n b sc) debug =

@@ -1228,7 +1243,7 @@ prettyEnv env t = prettyEnv' env t False

1228 -- Render a `Binder` and its name

1243 -- Render a `Binder` and its name

1229 prettySb env n (Lam t) = prettyB env "λ" "=>" n t

1244 prettySb env n (Lam t) = prettyB env "λ" "=>" n t

1230 prettySb env n (Hole t) = prettyB env "?defer" "." n t

1245 prettySb env n (Hole t) = prettyB env "?defer" "." n t

1231− prettySb env n (Pi t) = prettyB env "(" ") ->" n t

1246+ prettySb env n (Pi t _) = prettyB env "(" ") ->" n t

1232 prettySb env n (PVar t) = prettyB env "pat" "." n t

1247 prettySb env n (PVar t) = prettyB env "pat" "." n t

1233 prettySb env n (PVTy t) = prettyB env "pty" "." n t

1248 prettySb env n (PVTy t) = prettyB env "pty" "." n t

1234 prettySb env n (Let t v) = prettyBv env "let" "in" n t v

1249 prettySb env n (Let t v) = prettyBv env "let" "in" n t v

@@ -1254,8 +1269,10 @@ showEnv' env t dbg = se 10 env t where

1254 = (show $ fst $ env!!i) ++

1269 = (show $ fst $ env!!i) ++

1255 if dbg then "{" ++ show i ++ "}" else ""

1270 if dbg then "{" ++ show i ++ "}" else ""

1256 | otherwise = "!!V " ++ show i ++ "!!"

1271 | otherwise = "!!V " ++ show i ++ "!!"

1257− se p env (Bind n b@(Pi t) sc)

1272+ se p env (Bind n b@(Pi t k) sc)

1258− | noOccurrence n sc && not dbg = bracket p 2 $ se 1 env t ++ " -> " ++ se 10 ((n,b):env) sc

1273+ | noOccurrence n sc && not dbg = bracket p 2 $ se 1 env t ++ arrow k ++ se 10 ((n,b):env) sc

1274+ where arrow (TType _) = " -> "

1275+ arrow u = " [" ++ show u ++ "] -> "

1259 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

1276 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

1260 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

1277 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

1261 se p env (Proj x i) = se 1 env x ++ "!" ++ show i

1278 se p env (Proj x i) = se 1 env x ++ "!" ++ show i

@@ -1268,7 +1285,7 @@ showEnv' env t dbg = se 10 env t where

1268 sb env n (Lam t) = showb env "\\ " " => " n t

1285 sb env n (Lam t) = showb env "\\ " " => " n t

1269 sb env n (Hole t) = showb env "? " ". " n t

1286 sb env n (Hole t) = showb env "? " ". " n t

1270 sb env n (GHole i t) = showb env "?defer " ". " n t

1287 sb env n (GHole i t) = showb env "?defer " ". " n t

1271− sb env n (Pi t) = showb env "(" ") -> " n t

1288+ sb env n (Pi t _) = showb env "(" ") -> " n t

1272 sb env n (PVar t) = showb env "pat " ". " n t

1289 sb env n (PVar t) = showb env "pat " ". " n t

1273 sb env n (PVTy t) = showb env "pty " ". " n t

1290 sb env n (PVTy t) = showb env "pty " ". " n t

1274 sb env n (Let t v) = showbv env "let " " in " n t v

1291 sb env n (Let t v) = showbv env "let " " in " n t v

@@ -1328,7 +1345,7 @@ orderPats tm = op [] tm

1328

1345

1329 op ps (Bind n (PVar t) sc) = op ((n, PVar t) : ps) sc

1346 op ps (Bind n (PVar t) sc) = op ((n, PVar t) : ps) sc

1330 op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc

1347 op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc

1331− op ps (Bind n (Pi t) sc) = op ((n, Pi t) : ps) sc

1348+ op ps (Bind n (Pi t k) sc) = op ((n, Pi t k) : ps) sc

1332 op ps sc = bindAll (sortP ps) sc

1349 op ps sc = bindAll (sortP ps) sc

1333

1350

1334 sortP ps = pick [] (reverse ps)

1351 sortP ps = pick [] (reverse ps)

@@ -1373,9 +1390,10 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in

1373 v' <- getPats v

1390 v' <- getPats v

1374 sc' <- getPats sc

1391 sc' <- getPats sc

1375 return (Bind n (Let t' v') sc')

1392 return (Bind n (Let t' v') sc')

1376− getPats (Bind n (Pi t) sc) = do t' <- getPats t

1393+ getPats (Bind n (Pi t k) sc) = do t' <- getPats t

1394+ k' <- getPats k

1377− sc' <- getPats sc

1395+ sc' <- getPats sc

1378− return (Bind n (Pi t') sc')

1396+ return (Bind n (Pi t' k') sc')

1379 getPats (Bind n (Lam t) sc) = do t' <- getPats t

1397 getPats (Bind n (Lam t) sc) = do t' <- getPats t

1380 sc' <- getPats sc

1398 sc' <- getPats sc

1381 return (Bind n (Lam t') sc')

1399 return (Bind n (Lam t') sc')

src/Idris/Core/Typecheck.hs+95−62

@@ -69,42 +69,51 @@ check ctxt env tm

69 = evalStateT (check' True ctxt env tm) (0, []) -- Holes allowed

70

71check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

72−check' holes ctxt env top = chk env top where

72+check' holes ctxt env top = chk (TType (UVar 0)) env top where

73+

74+ smaller (UType NullType) _ = UType NullType

75+ smaller _ (UType NullType) = UType NullType

76+ smaller (UType u) _ = UType u

77+ smaller _ (UType u) = UType u

78+ smaller x _ = x

79+

80+ chk :: Type -> -- uniqueness level

81+ Env -> Raw -> StateT UCs TC (Term, Type)

73− chk env (Var n)

82+ chk u env (Var n)

74 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

83 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

75 | (P nt n' ty : _) <- lookupP n ctxt = return (P nt n' ty, ty)

84 | (P nt n' ty : _) <- lookupP n ctxt = return (P nt n' ty, ty)

76 | otherwise = do lift $ tfail $ NoSuchVariable n

85 | otherwise = do lift $ tfail $ NoSuchVariable n

77− chk env (RApp f a)

86+ chk u env ap@(RApp f a)

78− = do (fv, fty) <- chk env f

87+ = do (fv, fty) <- chk u env f

79− (av, aty) <- chk env a

88+ (av, aty) <- chk u env a

80 let fty' = case uniqueBinders (map fst env) (finalise fty) of

89 let fty' = case uniqueBinders (map fst env) (finalise fty) of

81− ty@(Bind x (Pi s) t) -> ty

90+ ty@(Bind x (Pi s k) t) -> ty

82 _ -> uniqueBinders (map fst env)

91 _ -> uniqueBinders (map fst env)

83 $ case hnf ctxt env fty of

92 $ case hnf ctxt env fty of

84− ty@(Bind x (Pi s) t) -> ty

93+ ty@(Bind x (Pi s k) t) -> ty

85 _ -> normalise ctxt env fty

94 _ -> normalise ctxt env fty

86 case fty' of

95 case fty' of

87− Bind x (Pi s) t ->

96+ Bind x (Pi s k) t ->

88 do convertsC ctxt env aty s

97 do convertsC ctxt env aty s

89 let apty = simplify initContext env

98 let apty = simplify initContext env

90 (Bind x (Let aty av) t)

99 (Bind x (Let aty av) t)

91 return (App fv av, apty)

100 return (App fv av, apty)

92 t -> lift $ tfail $ NonFunctionType fv fty

101 t -> lift $ tfail $ NonFunctionType fv fty

93− chk env RType

102+ chk u env RType

94 | holes = return (TType (UVal 0), TType (UVal 0))

103 | holes = return (TType (UVal 0), TType (UVal 0))

95 | otherwise = do (v, cs) <- get

104 | otherwise = do (v, cs) <- get

96 let c = ULT (UVar v) (UVar (v+1))

105 let c = ULT (UVar v) (UVar (v+1))

97 put (v+2, (c:cs))

106 put (v+2, (c:cs))

98 return (TType (UVar v), TType (UVar (v+1)))

107 return (TType (UVar v), TType (UVar (v+1)))

99− chk env (RUType u)

108+ chk u env (RUType un)

100− | holes = return (UType u, TType (UVal 0))

109+ | holes = return (UType un, TType (UVal 0))

101 | otherwise = do -- TODO! (v, cs) <- get

110 | otherwise = do -- TODO! (v, cs) <- get

102 -- let c = ULT (UVar v) (UVar (v+1))

111 -- let c = ULT (UVar v) (UVar (v+1))

103 -- put (v+2, (c:cs))

112 -- put (v+2, (c:cs))

104 -- return (TType (UVar v), TType (UVar (v+1)))

113 -- return (TType (UVar v), TType (UVar (v+1)))

105− return (UType u, TType (UVal 0))

114+ return (UType un, TType (UVal 0))

106− chk env (RConstant Forgot) = return (Erased, Erased)

115+ chk u env (RConstant Forgot) = return (Erased, Erased)

107− chk env (RConstant c) = return (Constant c, constType c)

116+ chk u env (RConstant c) = return (Constant c, constType c)

108 where constType (I _) = Constant (AType (ATInt ITNative))

117 where constType (I _) = Constant (AType (ATInt ITNative))

109 constType (BI _) = Constant (AType (ATInt ITBig))

118 constType (BI _) = Constant (AType (ATInt ITBig))

110 constType (Fl _) = Constant (AType ATFloat)

119 constType (Fl _) = Constant (AType ATFloat)

@@ -120,107 +129,122 @@ check' holes ctxt env top = chk env top where

120 constType (B64V a) = Constant (AType (ATInt (ITVec IT64 (V.length a))))

129 constType (B64V a) = Constant (AType (ATInt (ITVec IT64 (V.length a))))

121 constType Forgot = Erased

130 constType Forgot = Erased

122 constType _ = TType (UVal 0)

131 constType _ = TType (UVal 0)

123− chk env (RForce t) = do (_, ty) <- chk env t

132+ chk u env (RForce t) = do (_, ty) <- chk u env t

124− return (Erased, ty)

133+ return (Erased, ty)

125− chk env (RBind n (Pi s) t)

134+ chk u env (RBind n (Pi s k) t)

126− = do (sv, st) <- chk env s

135+ = do (sv, st) <- chk u env s

136+ (kv, kt) <- chk u env k

127− (tv, tt) <- chk ((n, Pi sv) : env) t

137+ (tv, tt) <- chk st ((n, Pi sv kv) : env) t

138+-- let tv = mkUniquePi kv tv_in

128 (v, cs) <- get

139 (v, cs) <- get

129 case (normalise ctxt env st, normalise ctxt env tt) of

140 case (normalise ctxt env st, normalise ctxt env tt) of

130 (TType su, TType tu) -> do

141 (TType su, TType tu) -> do

131 when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)

142 when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)

132− return (Bind n (Pi (uniqueBinders (map fst env) sv))

143+ let k' = u `smaller` st `smaller` kv `smaller` TType (UVar v)

133− (pToV n tv), TType (UVar v))

144+ return (Bind n (Pi (uniqueBinders (map fst env) sv) k')

134− (u, u') ->

145+ (pToV n tv), k')

146+ (un, un') ->

147+ let k' = u `smaller` st `smaller` kv `smaller` un `smaller` un' in

135− return (Bind n (Pi (uniqueBinders (map fst env) sv))

148+ return (Bind n (Pi (uniqueBinders (map fst env) sv) k')

136− (pToV n tv), smaller u u')

149+ (pToV n tv), k')

150+

151+ where mkUniquePi kv (Bind n (Pi s k) sc)

152+ = let k' = smaller kv k in

153+ Bind n (Pi s k') (mkUniquePi k' sc)

154+ mkUniquePi kv (Bind n (Lam t) sc)

155+ = Bind n (Lam (mkUniquePi kv t)) (mkUniquePi kv sc)

156+ mkUniquePi kv (Bind n (Let t v) sc)

157+ = Bind n (Let (mkUniquePi kv t) v) (mkUniquePi kv sc)

158+ mkUniquePi kv t = t

159+

160+ -- Kind of the whole thing is the kind of the most unique thing

161+ -- in the environment (because uniqueness taints everything...)

162+ mostUnique [] k = k

163+ mostUnique (Pi _ pk : es) k = mostUnique es (smaller pk k)

164+ mostUnique (_ : es) k = mostUnique es k

137

165

138− where smaller (UType NullType) _ = UType NullType

139− smaller _ (UType NullType) = UType NullType

140− smaller (UType u) _ = UType u

141− smaller _ (UType u) = UType u

142− chk env (RBind n b sc)

166+ chk u env (RBind n b sc)

143− = do b' <- checkBinder b

167+ = do (b', bt') <- checkBinder b

144− (scv, sct) <- chk ((n, b'):env) sc

168+ (scv, sct) <- chk (smaller bt' u) ((n, b'):env) sc

145− discharge n b' (pToV n scv) (pToV n sct)

169+ discharge n b' bt' (pToV n scv) (pToV n sct)

146 where checkBinder (Lam t)

170 where checkBinder (Lam t)

147− = do (tv, tt) <- chk env t

171+ = do (tv, tt) <- chk u env t

148 let tv' = normalise ctxt env tv

172 let tv' = normalise ctxt env tv

149 let tt' = normalise ctxt env tt

173 let tt' = normalise ctxt env tt

150 lift $ isType ctxt env tt'

174 lift $ isType ctxt env tt'

151− return (Lam tv)

175+ return (Lam tv, tt')

152 checkBinder (Let t v)

176 checkBinder (Let t v)

153− = do (tv, tt) <- chk env t

177+ = do (tv, tt) <- chk u env t

154− (vv, vt) <- chk env v

178+ (vv, vt) <- chk u env v

155 let tv' = normalise ctxt env tv

179 let tv' = normalise ctxt env tv

156 let tt' = normalise ctxt env tt

180 let tt' = normalise ctxt env tt

157 convertsC ctxt env vt tv

181 convertsC ctxt env vt tv

158 lift $ isType ctxt env tt'

182 lift $ isType ctxt env tt'

159− return (Let tv vv)

183+ return (Let tv vv, tt')

160 checkBinder (NLet t v)

184 checkBinder (NLet t v)

161− = do (tv, tt) <- chk env t

185+ = do (tv, tt) <- chk u env t

162− (vv, vt) <- chk env v

186+ (vv, vt) <- chk u env v

163 let tv' = normalise ctxt env tv

187 let tv' = normalise ctxt env tv

164 let tt' = normalise ctxt env tt

188 let tt' = normalise ctxt env tt

165 convertsC ctxt env vt tv

189 convertsC ctxt env vt tv

166 lift $ isType ctxt env tt'

190 lift $ isType ctxt env tt'

167− return (NLet tv vv)

191+ return (NLet tv vv, tt')

168 checkBinder (Hole t)

192 checkBinder (Hole t)

169 | not holes = lift $ tfail (IncompleteTerm undefined)

193 | not holes = lift $ tfail (IncompleteTerm undefined)

170 | otherwise

194 | otherwise

171− = do (tv, tt) <- chk env t

195+ = do (tv, tt) <- chk u env t

172 let tv' = normalise ctxt env tv

196 let tv' = normalise ctxt env tv

173 let tt' = normalise ctxt env tt

197 let tt' = normalise ctxt env tt

174 lift $ isType ctxt env tt'

198 lift $ isType ctxt env tt'

175− return (Hole tv)

199+ return (Hole tv, tt')

176 checkBinder (GHole i t)

200 checkBinder (GHole i t)

177− = do (tv, tt) <- chk env t

201+ = do (tv, tt) <- chk u env t

178 let tv' = normalise ctxt env tv

202 let tv' = normalise ctxt env tv

179 let tt' = normalise ctxt env tt

203 let tt' = normalise ctxt env tt

180 lift $ isType ctxt env tt'

204 lift $ isType ctxt env tt'

181− return (GHole i tv)

205+ return (GHole i tv, tt')

182 checkBinder (Guess t v)

206 checkBinder (Guess t v)

183 | not holes = lift $ tfail (IncompleteTerm undefined)

207 | not holes = lift $ tfail (IncompleteTerm undefined)

184 | otherwise

208 | otherwise

185− = do (tv, tt) <- chk env t

209+ = do (tv, tt) <- chk u env t

186− (vv, vt) <- chk env v

210+ (vv, vt) <- chk u env v

187 let tv' = normalise ctxt env tv

211 let tv' = normalise ctxt env tv

188 let tt' = normalise ctxt env tt

212 let tt' = normalise ctxt env tt

189 convertsC ctxt env vt tv

213 convertsC ctxt env vt tv

190 lift $ isType ctxt env tt'

214 lift $ isType ctxt env tt'

191− return (Guess tv vv)

215+ return (Guess tv vv, tt')

192 checkBinder (PVar t)

216 checkBinder (PVar t)

193− = do (tv, tt) <- chk env t

217+ = do (tv, tt) <- chk u env t

194 let tv' = normalise ctxt env tv

218 let tv' = normalise ctxt env tv

195 let tt' = normalise ctxt env tt

219 let tt' = normalise ctxt env tt

196 lift $ isType ctxt env tt'

220 lift $ isType ctxt env tt'

197 -- Normalised version, for erasure purposes (it's easier

221 -- Normalised version, for erasure purposes (it's easier

198 -- to tell if it's a collapsible variable)

222 -- to tell if it's a collapsible variable)

199− return (PVar tv)

223+ return (PVar tv, tt')

200 checkBinder (PVTy t)

224 checkBinder (PVTy t)

201− = do (tv, tt) <- chk env t

225+ = do (tv, tt) <- chk u env t

202 let tv' = normalise ctxt env tv

226 let tv' = normalise ctxt env tv

203 let tt' = normalise ctxt env tt

227 let tt' = normalise ctxt env tt

204 lift $ isType ctxt env tt'

228 lift $ isType ctxt env tt'

205− return (PVTy tv)

229+ return (PVTy tv, tt')

206

230

207− discharge n (Lam t) scv sct

231+ discharge n (Lam t) bt scv sct

208− = return (Bind n (Lam t) scv, Bind n (Pi t) sct)

232+ = return (Bind n (Lam t) scv, Bind n (Pi t bt) sct)

209− discharge n (Pi t) scv sct

233+ discharge n (Pi t k) bt scv sct

210− = return (Bind n (Pi t) scv, sct)

234+ = return (Bind n (Pi t k) scv, sct)

211− discharge n (Let t v) scv sct

235+ discharge n (Let t v) bt scv sct

212 = return (Bind n (Let t v) scv, Bind n (Let t v) sct)

236 = return (Bind n (Let t v) scv, Bind n (Let t v) sct)

213− discharge n (NLet t v) scv sct

237+ discharge n (NLet t v) bt scv sct

214 = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)

238 = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)

215− discharge n (Hole t) scv sct

239+ discharge n (Hole t) bt scv sct

216 = return (Bind n (Hole t) scv, sct)

240 = return (Bind n (Hole t) scv, sct)

217− discharge n (GHole i t) scv sct

241+ discharge n (GHole i t) bt scv sct

218 = return (Bind n (GHole i t) scv, sct)

242 = return (Bind n (GHole i t) scv, sct)

219− discharge n (Guess t v) scv sct

243+ discharge n (Guess t v) bt scv sct

220 = return (Bind n (Guess t v) scv, sct)

244 = return (Bind n (Guess t v) scv, sct)

221− discharge n (PVar t) scv sct

245+ discharge n (PVar t) bt scv sct

222 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)

246 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)

223− discharge n (PVTy t) scv sct

247+ discharge n (PVTy t) bt scv sct

224 = return (Bind n (PVTy t) scv, sct)

248 = return (Bind n (PVTy t) scv, sct)

225

249

226-- Number of times a name can be used

250-- Number of times a name can be used

@@ -257,11 +281,20 @@ checkUnique borrowed ctxt env tm

257 chkBinders env (App f a) = do chkBinders env f; chkBinders env a

281 chkBinders env (App f a) = do chkBinders env f; chkBinders env a

258 chkBinders env (Bind n b t)

282 chkBinders env (Bind n b t)

259 = do chkBinderName env n b

283 = do chkBinderName env n b

284+ -- Must be safe whether we evaluate the scope or binder first

285+ -- (Surely there is a tidier rule than this...?)

286+ st <- get

260 chkBinders ((n, b) : env) t

287 chkBinders ((n, b) : env) t

261 chkBinders env (binderTy b)

288 chkBinders env (binderTy b)

262 case b of

289 case b of

263 Let t v -> chkBinders env v

290 Let t v -> chkBinders env v

264 _ -> return ()

291 _ -> return ()

292+-- put st

293+-- chkBinders env (binderTy b)

294+-- case b of

295+-- Let t v -> chkBinders env v

296+-- _ -> return ()

297+-- chkBinders ((n, b) : env) t

265 chkBinders env t = return ()

298 chkBinders env t = return ()

266

299

267 chkBinderName :: Env -> Name -> Binder Term ->

300 chkBinderName :: Env -> Name -> Binder Term ->

src/Idris/Core/Unify.hs+11−11

@@ -84,12 +84,12 @@ match_unify ctxt env topx topy inj holes from =

84 -- but it scares me. However, matching is never guaranteed to give a unique

85 -- answer, merely a valid one, so perhaps we're okay.

86 -- In other words: it may vanish without warning some day :)

87− un names x tm@(App (P _ f (Bind fn (Pi t) sc)) a)

87+ un names x tm@(App (P _ f (Bind fn (Pi t _) sc)) a)

88 | (P (DCon _ _ _) _ _, _) <- unApply x,

89 holeIn env f || f `elem` holes

90 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

91 checkCycle names (f, Bind n' (Lam t) x)

92− un names tm@(App (P _ f (Bind fn (Pi t) sc)) a) x

92+ un names tm@(App (P _ f (Bind fn (Pi t _) sc)) a) x

93 | (P (DCon _ _ _) _ _, _) <- unApply x,

94 holeIn env f || f `elem` holes

95 = let n' = uniqueName fn (map fst env) in

@@ -133,7 +133,7 @@ match_unify ctxt env topx topy inj holes from =

133 h2 <- un bnames vx vy

134 combine bnames h1 h2

135 uB bnames (Lam tx) (Lam ty) = un bnames tx ty

136− uB bnames (Pi tx) (Pi ty) = un bnames tx ty

136+ uB bnames (Pi tx _) (Pi ty _) = un bnames tx ty

137 uB bnames x y = do UI s f <- get

138 let r = recoverable (normalise ctxt env (binderTy x))

139 (normalise ctxt env (binderTy y))

@@ -403,18 +403,18 @@ unify ctxt env topx topy inj holes usersupp from =

403 -- f D unifies with t -> D. This is dubious, but it helps with type

404 -- class resolution for type classes over functions.

405

406− un' fn bnames (App f x) (Bind n (Pi t) y)

406+ un' fn bnames (App f x) (Bind n (Pi t k) y)

407 | noOccurrence n y && injectiveApp f

408 = do ux <- un' False bnames x y

409 uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

410− (Bind n (Pi t) (V 1)))

410+ (Bind n (Pi t k) (V 1)))

411 combine bnames ux uf

412

413− un' fn bnames (Bind n (Pi t) y) (App f x)

413+ un' fn bnames (Bind n (Pi t k) y) (App f x)

414 | noOccurrence n y && injectiveApp f

415 = do ux <- un' False bnames y x

416 uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

417− (Bind n (Pi t) (V 1))) f

417+ (Bind n (Pi t k) (V 1))) f

418 combine bnames ux uf

419

420 un' fn bnames (Bind x bx sx) (Bind y by sy)

@@ -423,7 +423,7 @@ unify ctxt env topx topy inj holes usersupp from =

423 h2 <- un' False (((x,y),binderTy bx):bnames) sx sy

424 combine bnames h1 h2

425 where sameBinder (Lam _) (Lam _) = True

426− sameBinder (Pi _) (Pi _) = True

426+ sameBinder (Pi _ _) (Pi _ _) = True

427 sameBinder _ _ = False

428 un' fn bnames x y

429 | OK True <- convEq' ctxt holes x y = do sc 1; return []

@@ -551,7 +551,7 @@ unify ctxt env topx topy inj holes usersupp from =

551 sc 1

552 combine bnames h1 h2

553 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty

554− uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty

554+ uB bnames (Pi tx _) (Pi ty _) = do sc 1; un' False bnames tx ty

555 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty

556 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

557 uB bnames x y = do UI s f <- get

@@ -650,10 +650,10 @@ recoverable (App f a) (App f' a')

650 | f == f' = recoverable a a'

651recoverable (App f a) (App f' a')

652 = recoverable f f' -- && recoverable a a'

653−recoverable f (Bind _ (Pi _) sc)

653+recoverable f (Bind _ (Pi _ _) sc)

654 | (P (DCon _ _ _) _ _, _) <- unApply f = False

655 | (P (TCon _ _) _ _, _) <- unApply f = False

656−recoverable (Bind _ (Pi _) sc) f

656+recoverable (Bind _ (Pi _ _) sc) f

657 | (P (DCon _ _ _) _ _, _) <- unApply f = False

658 | (P (TCon _ _) _ _, _) <- unApply f = False

659recoverable (Bind _ (Lam _) sc) f = recoverable sc f

src/Idris/Coverage.hs+4−4

@@ -283,12 +283,12 @@ checkPositive mut_ns (cn, ty')

283 where

284 args t = [0..length (getArgTys t)-1]

285

286− cp (Bind n (Pi aty) sc) = posArg aty && cp sc

286+ cp (Bind n (Pi aty _) sc) = posArg aty && cp sc

287 cp t | (P _ n' _, args) <- unApply t,

288 n' `elem` mut_ns = all noRec args

289 cp _ = True

290

291− posArg (Bind _ (Pi nty) sc)

291+ posArg (Bind _ (Pi nty _) sc)

292 | (P _ n' _, args) <- unApply nty

293 = n' `notElem` mut_ns && all noRec args && posArg sc

294 posArg t | (P _ n' _, args) <- unApply t,

@@ -531,8 +531,8 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

531 = case lookupTy n (tt_ctxt ist) of

532 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args

533 _ -> args

534− where expand i (Bind n (Pi _) sc) (x : xs) = x : expand (i + 1) sc xs

534+ where expand i (Bind n (Pi _ _) sc) (x : xs) = x : expand (i + 1) sc xs

535− expand i (Bind n (Pi _) sc) [] = Just (i, Same) : expand (i + 1) sc []

535+ expand i (Bind n (Pi _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []

536 expand i _ xs = xs

537

538 mkChange n args pargs = [(n, expandToArity n (sizes args))]

src/Idris/Delaborate.hs+15−7

@@ -58,18 +58,18 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

58 _ -> PRef un n

59 de env _ (Bind n (Lam ty) sc)

60 = PLam n (de env [] ty) (de ((n,n):env) [] sc)

61− de env ((PImp { argopts = opts }):is) (Bind n (Pi ty) sc)

61+ de env ((PImp { argopts = opts }):is) (Bind n (Pi ty _) sc)

62 = PPi (Imp opts Dynamic False) n (de env [] ty) (de ((n,n):env) is sc)

63− de env (PConstraint _ _ _ _:is) (Bind n (Pi ty) sc)

63+ de env (PConstraint _ _ _ _:is) (Bind n (Pi ty _) sc)

64 = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)

65− de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi ty) sc)

65+ de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi ty _) sc)

66 = PPi (tacimpl tac) n (de env [] ty) (de ((n,n):env) is sc)

67− de env (plic:is) (Bind n (Pi ty) sc)

67+ de env (plic:is) (Bind n (Pi ty _) sc)

68 = PPi (Exp (argopts plic) Dynamic False)

69 n

70 (de env [] ty)

71 (de ((n,n):env) is sc)

72− de env [] (Bind n (Pi ty) sc)

72+ de env [] (Bind n (Pi ty _) sc)

73 = PPi expl n (de env [] ty) (de ((n,n):env) [] sc)

74 de env _ (Bind n (Let ty val) sc)

75 = PLet n (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

@@ -183,10 +183,18 @@ pprintErr' i (CantUnify _ x_in y_in e sc s) =

183 if (opt_errContext (idris_options i)) then showSc i sc else empty

184pprintErr' i (CantConvert x y env) =

185 text "Can't convert" <>

186− indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x))) <$>

186+ indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

187+ (delab i (flagUnique x)))) <$>

187 text "with" <>

188 text "with" <>

188− indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i y))) <>

189+ indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

190+ (delab i (flagUnique y)))) <>

189 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

191 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

192+ where flagUnique (Bind n (Pi t k@(UType u)) sc)

193+ = App (P Ref (sUN (show u)) Erased)

194+ (Bind n (Pi (flagUnique t) k) (flagUnique sc))

195+ flagUnique (App f a) = App (flagUnique f) (flagUnique a)

196+ flagUnique (Bind n b sc) = Bind n (fmap flagUnique b) (flagUnique sc)

197+ flagUnique t = t

190pprintErr' i (CantSolveGoal x env) =

198pprintErr' i (CantSolveGoal x env) =

191 text "Can't solve goal " <>

199 text "Can't solve goal " <>

192 indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x))) <>

200 indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x))) <>

src/Idris/Elab/Clause.hs+3−3

@@ -248,7 +248,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

248 force (normalisePats ctxt [] y))

249 simple_lhs ctxt t = t

250

251− simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p

251+ simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p

252 (rt_simplify ctxt [] y)))

253

254 -- this is so pattern types are in the right form for erasure

@@ -741,7 +741,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

741 let wargval = getRetTy cwvalN

742 let wargtype = getRetTy cwvaltyN

743 logLvl 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)

744− let wtype = bindTyArgs Pi (bargs_pre ++

744+ let wtype = bindTyArgs (flip Pi (TType (UVar 0))) (bargs_pre ++

745 (sMN 0 "warg", wargtype) :

746 map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)

747 (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)

@@ -789,7 +789,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

789 (crhs, crhsty) <- recheckC fc [] rhs'

790 return $ (Right (clhs, crhs), lhs)

791 where

792− getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

792+ getImps (Bind n (Pi _ _) t) = pexp Placeholder : getImps t

793 getImps _ = []

794

795 mkAuxC wname lhs ns ns' (PClauses fc o n cs)

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

@@ -168,7 +168,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

168 getDataApp f@(App _ _)

169 | (P _ d _, args) <- unApply f

170 = if (d == n) then [mParam args args] else []

171− getDataApp (Bind n (Pi t) sc)

171+ getDataApp (Bind n (Pi t _) sc)

172 = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)

173 getDataApp _ = []

174

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

@@ -101,11 +101,11 @@ buildType info syn fc opts n ty' = do

101

102 return (cty, ckind, ty, inacc)

103 where

104− patToImp (Bind n (PVar t) sc) = Bind n (Pi t) (patToImp sc)

104+ patToImp (Bind n (PVar t) sc) = Bind n (Pi t (TType (UVar 0))) (patToImp sc)

105 patToImp (Bind n b sc) = Bind n b (patToImp sc)

106 patToImp t = t

107

108− param_pos i ns (Bind n (Pi t) sc)

108+ param_pos i ns (Bind n (Pi t _) sc)

109 | n `elem` ns = i : param_pos (i + 1) ns sc

110 | otherwise = param_pos (i + 1) ns sc

111 param_pos i ns t = []

@@ -189,7 +189,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

189 lst = txt "List"

190 errrep = txt "ErrorReportPart"

191

192− tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _))

192+ tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _) _)

193 (App (P _ (NS (UN m) ns2) _)

194 (App (P _ (NS (UN l) ns3) _)

195 (P _ (NS (UN r) ns4) _))))

src/Idris/Elab/Utils.hs+4−4

@@ -46,7 +46,7 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

46-- Get the list of (index, name) of inaccessible arguments from an elaborated

47-- type

48inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

49−inaccessibleImps i (Bind n (Pi t) sc) (inacc : ins)

49+inaccessibleImps i (Bind n (Pi t _) sc) (inacc : ins)

50 | inacc = (i, n) : inaccessibleImps (i + 1) sc ins

51 | otherwise = inaccessibleImps (i + 1) sc ins

52inaccessibleImps _ _ _ = []

@@ -152,10 +152,10 @@ psolve tm = return ()

152pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc

153pvars ist _ = []

154

155−getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

155+getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t _) sc)

156 = nub $ getFixedInType i env [] t ++

157 getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

158−getFixedInType i env (_ : is) (Bind n (Pi t) sc)

158+getFixedInType i env (_ : is) (Bind n (Pi t _) sc)

159 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

160getFixedInType i env is tm@(App f a)

161 | (P _ tn _, args) <- unApply tm

@@ -169,7 +169,7 @@ getFixedInType i env is tm@(App f a)

169 getFixedInType i env is a

170getFixedInType i _ _ _ = []

171

172−getFlexInType i env ps (Bind n (Pi t) sc)

172+getFlexInType i env ps (Bind n (Pi t _) sc)

173 = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++

174 getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)

175getFlexInType i env ps tm@(App f a)

src/Idris/ElabDecls.hs+7−7

@@ -103,9 +103,9 @@ elabPrims = do mapM_ (elabDecl' EAll recinfo)

103

104 p_believeMe [_,_,x] = Just x

105 p_believeMe _ = Nothing

106− believeTy = Bind (sUN "a") (Pi (TType (UVar (-2))))

106+ believeTy = Bind (sUN "a") (Pi (TType (UVar (-2))) (TType (UVar 0)))

107− (Bind (sUN "b") (Pi (TType (UVar (-2))))

107+ (Bind (sUN "b") (Pi (TType (UVar (-2))) (TType (UVar 0)))

108− (Bind (sUN "x") (Pi (V 1)) (V 1)))

108+ (Bind (sUN "x") (Pi (V 1) (TType (UVar 0))) (V 1)))

109 elabBelieveMe

110 = do let prim__believe_me = sUN "prim__believe_me"

111 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

@@ -126,10 +126,10 @@ elabPrims = do mapM_ (elabDecl' EAll recinfo)

126 vnNothing = VP (DCon 0 1 False) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased

127 vnRefl = VP (DCon 0 2 False) eqCon VErased

128

129− synEqTy = Bind (sUN "a") (Pi (TType (UVar (-3))))

129+ synEqTy = Bind (sUN "a") (Pi (TType (UVar (-3))) (TType (UVar 0)))

130− (Bind (sUN "b") (Pi (TType (UVar (-3))))

130+ (Bind (sUN "b") (Pi (TType (UVar (-3))) (TType (UVar 0)))

131− (Bind (sUN "x") (Pi (V 1))

131+ (Bind (sUN "x") (Pi (V 1) (TType (UVar 0)))

132− (Bind (sUN "y") (Pi (V 1))

132+ (Bind (sUN "y") (Pi (V 1) (TType (UVar 0)))

133 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)

134 [V 3, V 2, V 1, V 0]]))))

135 elabSynEq

src/Idris/ElabTerm.hs+10−9

@@ -472,7 +472,7 @@ elab ist info emode opts fn tm

472 ans <- claimArgTys env xs

473 return ((aval, (True, (Var an))) : ans)

474 fnTy [] ret = forget ret

475− fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi xt) (fnTy xs ret)

475+ fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi xt RType) (fnTy xs ret)

476

477 localVar env (PRef _ x)

478 = case lookup x env of

@@ -1372,9 +1372,9 @@ runTac autoSolve ist fn tac

1372 where tacticTy = Var (reflm "Tactic")

1373 listTy = Var (sNS (sUN "List") ["List", "Prelude"])

1374 scriptTy = (RBind (sMN 0 "__pi_arg")

1375− (Pi (RApp listTy envTupleType))

1375+ (Pi (RApp listTy envTupleType) RType)

1376 (RBind (sMN 1 "__pi_arg")

1377− (Pi (Var $ reflm "TT")) tacticTy))

1377+ (Pi (Var $ reflm "TT") RType) tacticTy))

1378 runT (ByReflection tm) -- run the reflection function 'tm' on the

1379 -- goal, then apply the resulting reflected Tactic

1380 = do tgoal <- goal

@@ -1624,8 +1624,8 @@ reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)

1624reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)

1625reifyTTBinderApp reif f [t]

1626 | f == reflm "Lam" = liftM Lam (reif t)

1627−reifyTTBinderApp reif f [t]

1627+reifyTTBinderApp reif f [t, k]

1628− | f == reflm "Pi" = liftM Pi (reif t)

1628+ | f == reflm "Pi" = liftM2 Pi (reif t) (reif k)

1629reifyTTBinderApp reif f [x, y]

1630 | f == reflm "Let" = liftM2 Let (reif x) (reif y)

1631reifyTTBinderApp reif f [x, y]

@@ -1768,9 +1768,10 @@ reflectQuotePattern unq (Bind n b x)

1768 fill $ reflCall "Lam" [Var (reflm "TT"), Var t']

1769 solve

1770 focus t'; reflectQuotePattern unq t

1771− reflectBinderQuotePattern unq (Pi t)

1771+ reflectBinderQuotePattern unq (Pi t k)

1772 = do t' <- claimTT (sMN 0 "ty") ; movelast t'

1773+ k' <- claimTT (sMN 0 "k"); movelast k';

1773− fill $ reflCall "Pi" [Var (reflm "TT"), Var t']

1774+ fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']

1774 solve

1775 solve

1775 focus t'; reflectQuotePattern unq t

1776 focus t'; reflectQuotePattern unq t

1776 reflectBinderQuotePattern unq (Let x y)

1777 reflectBinderQuotePattern unq (Let x y)

@@ -1917,8 +1918,8 @@ reflectBinder = reflectBinderQuote []

1917reflectBinderQuote :: [Name] -> Binder Term -> Raw

1918reflectBinderQuote :: [Name] -> Binder Term -> Raw

1918reflectBinderQuote unq (Lam t)

1919reflectBinderQuote unq (Lam t)

1919 = reflCall "Lam" [Var (reflm "TT"), reflectQuote unq t]

1920 = reflCall "Lam" [Var (reflm "TT"), reflectQuote unq t]

1920−reflectBinderQuote unq (Pi t)

1921+reflectBinderQuote unq (Pi t k)

1921− = reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t]

1922+ = reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t, reflectQuote unq k]

1922reflectBinderQuote unq (Let x y)

1923reflectBinderQuote unq (Let x y)

1923 = reflCall "Let" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]

1924 = reflCall "Let" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]

1924reflectBinderQuote unq (NLet x y)

1925reflectBinderQuote unq (NLet x y)

src/Idris/Erasure.hs+5−5

@@ -353,16 +353,16 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

353 -- dependencies of de bruijn variables are described in `bs'

354 getDepsTerm vs bs cd (V i) = snd (bs !! i) cd

355

356− getDepsTerm vs bs cd (Bind n bdr t)

356+ getDepsTerm vs bs cd (Bind n bdr body)

357 -- here we just push IM.empty on the de bruijn stack

358 -- the args will be marked as used at the usage site

359− | Lam ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd t

359+ | Lam ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd body

360− | Pi ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd t

360+ | Pi ty _ <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd body

361

362 -- let-bound variables can get partially evaluated

363 -- it is sufficient just to plug the Cond in when the bound names are used

364− | Let ty t <- bdr = getDepsTerm vs ((n, var t) : bs) cd t

364+ | Let ty t <- bdr = var t cd `union` getDepsTerm vs ((n, var t) : bs) cd body

365− | NLet ty t <- bdr = getDepsTerm vs ((n, var t) : bs) cd t

365+ | NLet ty t <- bdr = var t cd `union` getDepsTerm vs ((n, var t) : bs) cd body

366 where

367 var t cd = getDepsTerm vs bs cd t

368

src/Idris/IBC.hs+1−1

@@ -31,7 +31,7 @@ import Codec.Compression.Zlib (compress)

31import Util.Zlib (decompressEither)

32

33ibcVersion :: Word8

34−ibcVersion = 79

34+ibcVersion = 80

35

36data IBCFile = IBCFile { ver :: Word8,

37 sourcefile :: FilePath,

src/Idris/Interactive.hs+4−4

@@ -299,10 +299,10 @@ makeLemma fn updatefile l n

299 where getIndent s = length (takeWhile isSpace s)

300

301 appArgs skip 0 _ = ""

302− appArgs skip i (Bind n@(UN c) (Pi _) sc)

302+ appArgs skip i (Bind n@(UN c) (Pi _ _) sc)

303 | (thead c /= '_' && n `notElem` skip)

304 = " " ++ show n ++ appArgs skip (i - 1) sc

305− appArgs skip i (Bind _ (Pi _) sc) = appArgs skip (i - 1) sc

305+ appArgs skip i (Bind _ (Pi _ _) sc) = appArgs skip (i - 1) sc

306 appArgs skip i _ = ""

307

308 stripMNBind skip (PPi b n@(UN c) ty sc)

@@ -316,7 +316,7 @@ makeLemma fn updatefile l n

316 -- Make them implicit if they appear guarded by a top level constructor,

317 -- or at the top level themselves.

318 guessImps :: Context -> Term -> [Name]

319− guessImps ctxt (Bind n (Pi _) sc)

319+ guessImps ctxt (Bind n (Pi _ _) sc)

320 | guarded ctxt n (substV (P Bound n Erased) sc)

321 = n : guessImps ctxt sc

322 | otherwise = guessImps ctxt sc

@@ -328,7 +328,7 @@ makeLemma fn updatefile l n

328 isConName f ctxt = any (guarded ctxt n) args

329-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows

330-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc

331− guarded ctxt n (Bind _ (Pi t) sc)

331+ guarded ctxt n (Bind _ (Pi t _) sc)

332 = guarded ctxt n t || guarded ctxt n sc

333 guarded ctxt n _ = False

334

src/Idris/PartialEval.hs+13−12

@@ -35,35 +35,35 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

35 where

36 -- Specialise static argument in type by let-binding provided value instead

37 -- of expecting it as a function argument

38− st ((ExplicitS, v) : xs) (Bind n (Pi t) sc)

38+ st ((ExplicitS, v) : xs) (Bind n (Pi t _) sc)

39 = Bind n (Let t v) (st xs sc)

40− st ((ImplicitS, v) : xs) (Bind n (Pi t) sc)

40+ st ((ImplicitS, v) : xs) (Bind n (Pi t _) sc)

41 = Bind n (Let t v) (st xs sc)

42 -- Erase argument from function type

43− st ((UnifiedD, _) : xs) (Bind n (Pi t) sc)

43+ st ((UnifiedD, _) : xs) (Bind n (Pi t _) sc)

44 = st xs sc

45 -- Keep types as is

46− st (_ : xs) (Bind n (Pi t) sc)

46+ st (_ : xs) (Bind n (Pi t k) sc)

47− = Bind n (Pi t) (st xs sc)

47+ = Bind n (Pi t k) (st xs sc)

48 st _ t = t

49

50 -- Erase implicit dynamic argument if existing argument shares it value,

51 -- by substituting the value of previous argument

52− unifyEq (imp@(ImplicitD, v) : xs) (Bind n (Pi t) sc)

52+ unifyEq (imp@(ImplicitD, v) : xs) (Bind n (Pi t k) sc)

53 = do amap <- get

54 case lookup imp amap of

55 Just n' ->

56 do put (amap ++ [((UnifiedD, Erased), n)])

57 sc' <- unifyEq xs (subst n (P Bound n' Erased) sc)

58− return (Bind n (Pi t) sc') -- erase later

58+ return (Bind n (Pi t k) sc') -- erase later

59 _ -> do put (amap ++ [(imp, n)])

60 sc' <- unifyEq xs sc

61− return (Bind n (Pi t) sc')

61+ return (Bind n (Pi t k) sc')

62− unifyEq (x : xs) (Bind n (Pi t) sc)

62+ unifyEq (x : xs) (Bind n (Pi t k) sc)

63 = do args <- get

64 put (args ++ [(x, n)])

65 sc' <- unifyEq xs sc

66− return (Bind n (Pi t) sc')

66+ return (Bind n (Pi t k) sc')

67 unifyEq xs t = do args <- get

68 put (args ++ (zip xs (repeat (sUN "_"))))

69 return t

@@ -73,13 +73,14 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

73mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

74mkPE_TyDecl ist args ty = mkty args ty

75 where

76− mkty ((ExplicitD, v) : xs) (Bind n (Pi t) sc)

76+ mkty ((ExplicitD, v) : xs) (Bind n (Pi t k) sc)

77 = PPi expl n (delab ist t) (mkty xs sc)

78− mkty ((ImplicitD, v) : xs) (Bind n (Pi t) sc)

78+ mkty ((ImplicitD, v) : xs) (Bind n (Pi t k) sc)

79 | concreteClass ist t = mkty xs sc

80 | classConstraint ist t

81 = PPi constraint n (delab ist t) (mkty xs sc)

82 | otherwise = PPi impl n (delab ist t) (mkty xs sc)

83+

83 mkty (_ : xs) t

84 mkty (_ : xs) t

84 = mkty xs t

85 = mkty xs t

85 mkty [] t = delab ist t

86 mkty [] t = delab ist t

src/Idris/Primitives.hs+1−1

@@ -26,7 +26,7 @@ data Prim = Prim { p_name :: Name,

26

27ty :: [Const] -> Const -> Type

28ty [] x = Constant x

29−ty (t:ts) x = Bind (sMN 0 "T") (Pi (Constant t)) (ty ts x)

29+ty (t:ts) x = Bind (sMN 0 "T") (Pi (Constant t) (TType (UVar 0))) (ty ts x)

30

31total, partial, iopartial :: Totality

32total = Total []

src/Idris/REPL.hs+1−1

@@ -401,7 +401,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.Metavariables cols) =

401 -- | Split a function type into a pair of premises, conclusion.

402 -- Each maintains both the original and delaborated versions.

403 splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

404− splitPi ist (Bind n (Pi t) rest) =

404+ splitPi ist (Bind n (Pi t _) rest) =

405 let (hs, c, pc) = splitPi ist rest in

406 ((n, t, delabTy' ist [] t False False):hs,

407 c, delabTy' ist [] c False False)

src/Idris/TypeSearch.hs+2−2

@@ -112,7 +112,7 @@ computeDagP removePred t = (reverse (map f args), reverse removedArgs , retTy) w

112 (numArgs, args, removedArgs, retTy) = go 0 [] [] t

113

114 -- NOTE : args are in reverse order

115− go k args removedArgs (Bind n (Pi t) sc) = let arg = (n, t) in

115+ go k args removedArgs (Bind n (Pi t _) sc) = let arg = (n, t) in

116 if removePred t

117 then go k args (arg : removedArgs) sc

118 else go (succ k) (arg : args) removedArgs sc

@@ -346,7 +346,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

346 unifyQueue state [] = return state

347 unifyQueue state ((ty1, ty2) : queue) = do

348 --trace ("go: \n" ++ show state) True `seq` return ()

349− res <- tcToMaybe $ match_unify ctxt [ (n, Pi ty) | (n, ty) <- holes state] ty1 ty2 [] (map fst $ holes state) []

349+ res <- tcToMaybe $ match_unify ctxt [ (n, Pi ty (TType (UVar 0))) | (n, ty) <- holes state] ty1 ty2 [] (map fst $ holes state) []

350 (state', queueAdditions) <- resolveUnis res state

351 guard $ scoreCriterion (score state')

352 unifyQueue state' (queue ++ queueAdditions)

test/unique001/unique001.idr+1

@@ -25,6 +25,7 @@ showStuff xs = do

25 putStrLn (showU xs)

26 let xs' = umap (*2) xs

27 putStrLn (showU xs')

28+ putStrLn (showU xs')

28

29

29main : IO ()

30main : IO ()

30main = showStuff (mkUList 20)

31main = showStuff (mkUList 20)

test/unique001/unique001a.idr+40−4

@@ -19,13 +19,49 @@ mkUList : Nat -> UList Int

19mkUList Z = []

20mkUList (S k) = cast k :: mkUList k

21

22+-- showIt : UList Int -> Int -> String

23+-- showIt xs x = let xs' = umap (*2) xs in ""

24+

25+showIt : UList Int -> Int -> String

26+showIt [] y = "END"

27+showIt (x :: xs) y = let z = 0 :: xs in

28+ show x ++ "," ++ showU xs ++ showU z

29+

30+printThings : (Int -> String) -> IO ()

31+printThings f = do putStrLn (f 10)

32+ putStrLn (f 20)

33+

34+double : Int -> Int

35+double x = x * 2

36+

22showStuff : UList Int -> IO ()

37showStuff : UList Int -> IO ()

23showStuff xs = do

38showStuff xs = do

24 putStrLn (showU xs)

39 putStrLn (showU xs)

25− let xs' = umap (*2) xs

26 putStrLn (showU xs)

40 putStrLn (showU xs)

41+ -- xsFn gets a unique type since we're in a unique context

42+ -- now, but function built has a non-unique type

43+ (\xsFn : Int -> String =>

44+ do putStrLn "Hello"

45+ putStrLn (xsFn 42))

46+ (\dummy => showU (umap double xs))

47+

48+showStuff' : UList Int -> IO ()

49+showStuff' xs = do

50+ putStrLn (showU xs)

27− putStrLn (showU xs')

51+ putStrLn (showU xs)

52+ -- xsFn gets a unique type since we're in a unique context

53+ -- now, but function built has a non-unique type

54+ let xsFn = \dummy : Int => showU (umap double xs)

55+ putStrLn "Hello"

56+ putStrLn (xsFn 42)

57+ putStrLn (xsFn 42)

58+

59+showThings : UList Int -> IO ()

60+showThings xs = do

61+ putStrLn (showU xs)

62+ putStrLn (showU xs)

63+ -- showIt has a unique type, printThings wants a non-unique

64+ -- type

65+ printThings (showIt xs)

28

66

29−main : IO ()

30−main = showStuff (mkUList 20)

31

67