727b6a9 · Idris-dev · git.iko.soy

idris.cabal+6

@@ -510,6 +510,12 @@ Extra-source-files:

510510 test/unique001/run

511511 test/unique001/*.idr

512512 test/unique001/expected

513+ test/unique002/run

514+ test/unique002/*.idr

515+ test/unique002/expected

516+ test/unique003/run

517+ test/unique003/*.idr

518+ test/unique003/expected

513519

514520source-repository head

515521 type: git

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

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

9292||| Types annotations for bound variables in different

9393||| binding contexts

9494data Binder a = Lam a

95− | Pi a

95+ | Pi a a

9696 | Let a a

9797 | NLet a a

9898 | Hole a

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

104104

105105instance Functor Binder where

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

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

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

110110 map f (Hole x) = Hole (f x)

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

115115

116116instance Foldable Binder where

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

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

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

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

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

126126

127127instance Traversable Binder where

128128 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) |]

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

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

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

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

400400 instance Quotable (Binder TT) where

401401 quotedTy = `(Binder TT)

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

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

405406 ~(assert_total (quote y)))

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

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

431432

432433 quoteRawBinder : Binder Raw -> TT

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

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

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

437438 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

4848

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

5050binderTy (Lam t) = t

51−binderTy (Pi t) = t

51+binderTy (Pi t _) = t

5252binderTy (Let t1 t2) = t1

5353binderTy (NLet t1 t2) = t1

5454binderTy (Hole t) = t

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

160160

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

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

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

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

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

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

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

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

171171

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

173173 (Lam t) == (Lam t') = t == t'

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

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

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

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

177177 (Hole t) == (Hole t') = t == t'

src/Idris/AbsSyntax.hs+6−6

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

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

10661066 addIBC (IBCStatic n)

10671067 where

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

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

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

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

10711071 else if (not (searchArg p))

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

10731073 else (static, dynamic)

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

10751075

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

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

10771077 = nub $ freeArgNames ty

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

10791079 concatMap freeNames args

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

10851085 searchArg (TacImp _ _ _) = True

10861086 searchArg _ = False

10871087

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

10891089 staticList _ _ = []

10901090

10911091-- Dealing with implicit arguments

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

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

11871187 collectImps _ = []

11881188

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

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

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

11911191 where

11921192 argInfo n (Imp opt _ _) t'

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

12001200 argInfo n (TacImp opt _ scr) t'

12011201 = (InaccessibleArg `elem` opt,

12021202 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

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

12051205 getImps sc tm = []

12061206

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

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

16131613 su :: PTerm -> PTerm

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

16161616 = Placeholder

16171617 su (PApp fc fn args)

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

src/Idris/AbsSyntaxTree.hs+1−1

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

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

10511051

10521052getInferType (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))

10541054 toTy (PVar t) = PVTy t

10551055 toTy b = b

10561056getInferType (App (App _ ty) _) = ty

src/Idris/Apropos.hs+1−1

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

5353

5454instance Apropos (Binder (TT Name)) where

5555 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

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

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

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

176176 = case lookupTy n (tt_ctxt ist) of

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

178178 _ -> repeat Nothing

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

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

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

181181 | otherwise = Nothing

182182argTys _ _ = repeat Nothing

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

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

233233 = case x of

234234 Lam x1 -> do putWord8 0

235235 put x1

236− Pi x1 -> do putWord8 1

237− put x1

236+ Pi x1 x2 -> do putWord8 1

237+ put x1

238+ put x2

238239 Let x1 x2 -> do putWord8 2

239240 put x1

240241 put x2

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

259260 0 -> do x1 <- get

260261 return (Lam x1)

261262 1 -> do x1 <- get

262− return (Pi x1)

263+ x2 <- get

264+ return (Pi x1 x2)

263265 2 -> do x1 <- get

264266 x2 <- get

265267 return (Let x1 x2)

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

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

370370 toPat' [] (Constant VoidType) = PTyPat

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

372372

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

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

374374 | reflect && noOccurrence n sc

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

376376

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

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

7070

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

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

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

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

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

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

7676 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

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

255255 isInj ctxt (Constant _) = True

256256 isInj ctxt (TType _) = True

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

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

258258 isInj ctxt _ = False

259259

260260-- get instance argument names

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

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

455455 -> [Name] -- ^ Hypotheses

456456 -> 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 =

458458 do let t = rebind hs t_in

459459 n <- getNameFrom (mkMN n')

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

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

562562 priOrder _ Nothing = GT

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

564564

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

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

566566 do n <- unique_hole (mkMN n')

567567 when (null claims) (start_unify n)

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

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

597597checkPiGoal n

598598 = do g <- goal

599599 case g of

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

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

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

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

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

604604 claim a RType

605605 claim b RType

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

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

607607 movelast a

608608 movelast b

609609 fill (Var f)

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

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

619619 claim a RType

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

622622 tm <- get_term

623623 start_unify s

624624 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

239239 ev ntimes stk top env (V i)

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

241241 | 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

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

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

245246 wknV (-1) sc'

246−-- | otherwise

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

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

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

250−-- -- again when evaluation finished

251−-- hs <- get

252−-- let vd = nexthole hs

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

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

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

247+ | otherwise

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

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

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

251+ -- again when evaluation finished

252+ hs <- get

253+ let vd = nexthole hs

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

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

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

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

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

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

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

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

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

439440 | 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

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

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

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

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

580581 where

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

582583 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')

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

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

585587 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

8484 b' <- fixBinder b

8585 Bind n b' <$> toTT body'

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

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

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

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

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

9090 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' =

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

397397 where

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

400400

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

402402

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

515515 Just name -> name

516516 Nothing -> x

517517 let t' = case t of

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

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

519519 _ -> hnf ctxt env t

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

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

522522 case t' of

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

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

525− ps <- get

526− let (uh, uns) = unified ps

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

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

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

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

525+ ps <- get

526+ let (uh, uns) = unified ps

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

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

529529 _ -> lift $ tfail $ CantIntroduce t'

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

531531

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

535535 Just name -> name

536536 Nothing -> x

537537 let t' = case t of

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

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

539539 _ -> hnf ctxt env t

540540 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') $

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

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

544544 _ -> lift $ tfail $ CantIntroduce t'

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

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

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

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

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

554554

555555patvar :: Name -> RunTactic

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

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

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

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

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

643− | Pi { binderTy :: !b }

643+ | Pi { binderTy :: !b,

644+ binderKind :: !b }

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

645646 | Let { binderTy :: !b,

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

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

663664

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

665666 size (Lam ty) = 1 + size ty

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

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

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

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

669670 size (Hole ty) = 1 + size ty

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

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

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

679680fmapMB 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)

681682fmapMB 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)

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

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

685686

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

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

845846isInjective (Constant _) = True

846847isInjective (TType x) = True

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

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

848849isInjective (App f a) = isInjective f

849850isInjective _ = False

850851

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

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

10181019 st t = t

10191020

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+

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

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

10221037noOccurrence n t = no' 0 t

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

10431058

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

10451060arity :: TT n -> Int

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

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

10471062arity _ = 0

10481063

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

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

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

11021117getArgTys :: 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

11041119getArgTys _ = []

11051120

11061121getRetTy :: TT n -> TT n

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

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

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

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

11101125getRetTy sc = sc

11111126

11121127uniqueNameFrom :: [Name] -> [Name] -> Name

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

12121227 else

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

12141229 | 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

12161231 | noOccurrence n sc && not debug =

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

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

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

12281243 -- Render a `Binder` and its name

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

12301245 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

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

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

12341249 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

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

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

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

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

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

1272+ se p env (Bind n b@(Pi t k) 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 ++ "] -> "

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

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

12611278 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

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

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

12701287 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

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

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

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

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

13281345

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

13301347 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

13321349 op ps sc = bindAll (sortP ps) sc

13331350

13341351 sortP ps = pick [] (reverse ps)

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

13731390 v' <- getPats v

13741391 sc' <- getPats sc

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

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

1377− sc' <- getPats sc

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

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

1394+ k' <- getPats k

1395+ sc' <- getPats sc

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

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

13801398 sc' <- getPats sc

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

src/Idris/Core/Typecheck.hs+99−66

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

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

7070

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

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

73− chk env (Var n)

72+check' holes ctxt env top = chk (TType (UVar (-5))) 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)

82+ chk u env (Var n)

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

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

7685 | otherwise = do lift $ tfail $ NoSuchVariable n

77− chk env (RApp f a)

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

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

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

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

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

8089 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

8291 _ -> uniqueBinders (map fst env)

8392 $ case hnf ctxt env fty of

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

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

8594 _ -> normalise ctxt env fty

8695 case fty' of

87− Bind x (Pi s) t ->

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

8897 do convertsC ctxt env aty s

8998 let apty = simplify initContext env

9099 (Bind x (Let aty av) t)

91100 return (App fv av, apty)

92101 t -> lift $ tfail $ NonFunctionType fv fty

93− chk env RType

102+ chk u env RType

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

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

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

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

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

99− chk env (RUType u)

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

108+ chk u env (RUType un)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

121130 constType Forgot = Erased

122131 constType _ = TType (UVal 0)

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

124− return (Erased, ty)

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

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

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

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

133+ return (Erased, ty)

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

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

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

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

138+-- let tv = mkUniquePi kv tv_in

128139 (v, cs) <- get

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

130141 (TType su, TType tu) -> do

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

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

134− (u, u') ->

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

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

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

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

145+ (pToV n tv), k')

146+ (un, un') ->

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

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

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

137159

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)

143− = do b' <- checkBinder b

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

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

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

165+

166+ chk u env (RBind n b sc)

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

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

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

146170 where checkBinder (Lam t)

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

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

148172 let tv' = normalise ctxt env tv

149173 let tt' = normalise ctxt env tt

150174 lift $ isType ctxt env tt'

151− return (Lam tv)

175+ return (Lam tv, tt')

152176 checkBinder (Let t v)

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

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

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

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

155179 let tv' = normalise ctxt env tv

156180 let tt' = normalise ctxt env tt

157181 convertsC ctxt env vt tv

158182 lift $ isType ctxt env tt'

159− return (Let tv vv)

183+ return (Let tv vv, tt')

160184 checkBinder (NLet t v)

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

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

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

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

163187 let tv' = normalise ctxt env tv

164188 let tt' = normalise ctxt env tt

165189 convertsC ctxt env vt tv

166190 lift $ isType ctxt env tt'

167− return (NLet tv vv)

191+ return (NLet tv vv, tt')

168192 checkBinder (Hole t)

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

170194 | otherwise

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

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

172196 let tv' = normalise ctxt env tv

173197 let tt' = normalise ctxt env tt

174198 lift $ isType ctxt env tt'

175− return (Hole tv)

199+ return (Hole tv, tt')

176200 checkBinder (GHole i t)

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

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

178202 let tv' = normalise ctxt env tv

179203 let tt' = normalise ctxt env tt

180204 lift $ isType ctxt env tt'

181− return (GHole i tv)

205+ return (GHole i tv, tt')

182206 checkBinder (Guess t v)

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

184208 | otherwise

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

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

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

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

187211 let tv' = normalise ctxt env tv

188212 let tt' = normalise ctxt env tt

189213 convertsC ctxt env vt tv

190214 lift $ isType ctxt env tt'

191− return (Guess tv vv)

215+ return (Guess tv vv, tt')

192216 checkBinder (PVar t)

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

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

194218 let tv' = normalise ctxt env tv

195219 let tt' = normalise ctxt env tt

196220 lift $ isType ctxt env tt'

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

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

199− return (PVar tv)

223+ return (PVar tv, tt')

200224 checkBinder (PVTy t)

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

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

202226 let tv' = normalise ctxt env tv

203227 let tt' = normalise ctxt env tt

204228 lift $ isType ctxt env tt'

205− return (PVTy tv)

229+ return (PVTy tv, tt')

206230

207− discharge n (Lam t) scv sct

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

209− discharge n (Pi t) scv sct

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

211− discharge n (Let t v) scv sct

231+ discharge n (Lam t) bt scv sct

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

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

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

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

212236 = 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

214238 = 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

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

217− discharge n (GHole i t) scv sct

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

218242 = 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

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

221− discharge n (PVar t) scv sct

245+ discharge n (PVar t) bt scv sct

222246 = 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

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

225249

226250-- Number of times a name can be used

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

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

258282 chkBinders env (Bind n b t)

259283 = 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

287+ chkBinders env (binderTy b)

288+ case b of

289+ Let t v -> chkBinders env v

290+ _ -> return ()

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

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

261298 chkBinders env t = return ()

262299

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

@@ -275,10 +312,6 @@ checkUnique borrowed ctxt env tm

275312 UType AllTypes -> do ns <- get

276313 put ((n, (Once, AllTypes)) : ns)

277314 _ -> return ()

278− chkBinders env (binderTy b)

279− case b of

280− Let t v -> chkBinders env v

281− _ -> return ()

282315

283316 chkName n

284317 = do ns <- get

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

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

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

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

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

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

8989 holeIn env f || f `elem` holes

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

9191 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

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

9494 holeIn env f || f `elem` holes

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

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

133133 h2 <- un bnames vx vy

134134 combine bnames h1 h2

135135 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

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

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

139139 (normalise ctxt env (binderTy y))

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

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

404404 -- class resolution for type classes over functions.

405405

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)

407407 | noOccurrence n y && injectiveApp f

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

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

411411 combine bnames ux uf

412412

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)

414414 | noOccurrence n y && injectiveApp f

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

416416 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

418418 combine bnames ux uf

419419

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

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

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

424424 combine bnames h1 h2

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

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

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

427427 sameBinder _ _ = False

428428 un' fn bnames x y

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

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

551551 sc 1

552552 combine bnames h1 h2

553553 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

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

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

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

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

650650 | f == f' = recoverable a a'

651651recoverable (App f a) (App f' a')

652652 = recoverable f f' -- && recoverable a a'

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

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

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

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

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

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

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

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

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

src/Idris/Coverage.hs+4−4

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

283283 where

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

285285

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

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

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

288288 n' `elem` mut_ns = all noRec args

289289 cp _ = True

290290

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

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

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

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

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

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

531531 = case lookupTy n (tt_ctxt ist) of

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

533533 _ -> args

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 []

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 []

536536 expand i _ xs = xs

537537

538538 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

5858 _ -> PRef un n

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

6060 = 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)

6262 = 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)

6464 = 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)

6666 = 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)

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

6969 n

7070 (de env [] ty)

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

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

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

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

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

7575 = 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) =

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

184184pprintErr' i (CantConvert x y env) =

185185 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)))) <$>

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

189191 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

190198pprintErr' i (CantSolveGoal x env) =

191199 text "Can't solve goal " <>

192200 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

248248 force (normalisePats ctxt [] y))

249249 simple_lhs ctxt t = t

250250

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

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

252252 (rt_simplify ctxt [] y)))

253253

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

741741 let wargval = getRetTy cwvalN

742742 let wargtype = getRetTy cwvaltyN

743743 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 ++

745745 (sMN 0 "warg", wargtype) :

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

747747 (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)

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

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

791791 where

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

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

793793 getImps _ = []

794794

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

168168 getDataApp f@(App _ _)

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

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

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

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

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

173173 getDataApp _ = []

174174

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

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

101101

102102 return (cty, ckind, ty, inacc)

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

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

106106 patToImp t = t

107107

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

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

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

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

111111 param_pos i ns t = []

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

189189 lst = txt "List"

190190 errrep = txt "ErrorReportPart"

191191

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

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

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

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

195195 (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)

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

4747-- type

4848inaccessibleImps :: 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)

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

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

5252inaccessibleImps _ _ _ = []

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

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

153153pvars ist _ = []

154154

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

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

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

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

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

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

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

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

169169 getFixedInType i env is a

170170getFixedInType i _ _ _ = []

171171

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

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

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

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

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

src/Idris/ElabDecls.hs+7−7

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

103103

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

105105 p_believeMe _ = Nothing

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

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

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

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

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

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

109109 elabBelieveMe

110110 = do let prim__believe_me = sUN "prim__believe_me"

111111 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

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

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

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

128128

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

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

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

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

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

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

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

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

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

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

135135 elabSynEq

src/Idris/ElabTerm.hs+10−9

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

472472 ans <- claimArgTys env xs

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

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

476476

477477 localVar env (PRef _ x)

478478 = case lookup x env of

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

13721372 where tacticTy = Var (reflm "Tactic")

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

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

1375− (Pi (RApp listTy envTupleType))

1375+ (Pi (RApp listTy envTupleType) RType)

13761376 (RBind (sMN 1 "__pi_arg")

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

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

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

13791379 -- goal, then apply the resulting reflected Tactic

13801380 = do tgoal <- goal

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

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

16251625reifyTTBinderApp reif f [t]

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

1627−reifyTTBinderApp reif f [t]

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

1627+reifyTTBinderApp reif f [t, k]

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

16291629reifyTTBinderApp reif f [x, y]

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

16311631reifyTTBinderApp reif f [x, y]

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

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

17691769 solve

17701770 focus t'; reflectQuotePattern unq t

1771− reflectBinderQuotePattern unq (Pi t)

1771+ reflectBinderQuotePattern unq (Pi t k)

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

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

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

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

17741775 solve

17751776 focus t'; reflectQuotePattern unq t

17761777 reflectBinderQuotePattern unq (Let x y)

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

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

19181919reflectBinderQuote unq (Lam t)

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

1920−reflectBinderQuote unq (Pi t)

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

1921+reflectBinderQuote unq (Pi t k)

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

19221923reflectBinderQuote unq (Let x y)

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

19241925reflectBinderQuote 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]

353353 -- dependencies of de bruijn variables are described in `bs'

354354 getDepsTerm vs bs cd (V i) = snd (bs !! i) cd

355355

356− getDepsTerm vs bs cd (Bind n bdr t)

356+ getDepsTerm vs bs cd (Bind n bdr body)

357357 -- here we just push IM.empty on the de bruijn stack

358358 -- the args will be marked as used at the usage site

359− | Lam ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd t

360− | Pi 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 body

361361

362362 -- let-bound variables can get partially evaluated

363363 -- 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

365− | NLet 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 = var t cd `union` getDepsTerm vs ((n, var t) : bs) cd body

366366 where

367367 var t cd = getDepsTerm vs bs cd t

368368

src/Idris/IBC.hs+1−1

@@ -31,7 +31,7 @@ import Codec.Compression.Zlib (compress)

3131import Util.Zlib (decompressEither)

3232

3333ibcVersion :: Word8

34−ibcVersion = 79

34+ibcVersion = 80

3535

3636data IBCFile = IBCFile { ver :: Word8,

3737 sourcefile :: FilePath,

src/Idris/Interactive.hs+4−4

@@ -299,10 +299,10 @@ makeLemma fn updatefile l n

299299 where getIndent s = length (takeWhile isSpace s)

300300

301301 appArgs skip 0 _ = ""

302− appArgs skip i (Bind n@(UN c) (Pi _) sc)

302+ appArgs skip i (Bind n@(UN c) (Pi _ _) sc)

303303 | (thead c /= '_' && n `notElem` skip)

304304 = " " ++ 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

306306 appArgs skip i _ = ""

307307

308308 stripMNBind skip (PPi b n@(UN c) ty sc)

@@ -316,7 +316,7 @@ makeLemma fn updatefile l n

316316 -- Make them implicit if they appear guarded by a top level constructor,

317317 -- or at the top level themselves.

318318 guessImps :: Context -> Term -> [Name]

319− guessImps ctxt (Bind n (Pi _) sc)

319+ guessImps ctxt (Bind n (Pi _ _) sc)

320320 | guarded ctxt n (substV (P Bound n Erased) sc)

321321 = n : guessImps ctxt sc

322322 | otherwise = guessImps ctxt sc

@@ -328,7 +328,7 @@ makeLemma fn updatefile l n

328328 isConName f ctxt = any (guarded ctxt n) args

329329-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows

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

332332 = guarded ctxt n t || guarded ctxt n sc

333333 guarded ctxt n _ = False

334334

src/Idris/PartialEval.hs+13−12

@@ -35,35 +35,35 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

3535 where

3636 -- Specialise static argument in type by let-binding provided value instead

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

3939 = 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)

4141 = Bind n (Let t v) (st xs sc)

4242 -- Erase argument from function type

43− st ((UnifiedD, _) : xs) (Bind n (Pi t) sc)

43+ st ((UnifiedD, _) : xs) (Bind n (Pi t _) sc)

4444 = st xs sc

4545 -- Keep types as is

46− st (_ : xs) (Bind n (Pi t) sc)

47− = Bind n (Pi t) (st xs sc)

46+ st (_ : xs) (Bind n (Pi t k) sc)

47+ = Bind n (Pi t k) (st xs sc)

4848 st _ t = t

4949

5050 -- Erase implicit dynamic argument if existing argument shares it value,

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

5353 = do amap <- get

5454 case lookup imp amap of

5555 Just n' ->

5656 do put (amap ++ [((UnifiedD, Erased), n)])

5757 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

5959 _ -> do put (amap ++ [(imp, n)])

6060 sc' <- unifyEq xs sc

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

62− unifyEq (x : xs) (Bind n (Pi t) sc)

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

62+ unifyEq (x : xs) (Bind n (Pi t k) sc)

6363 = do args <- get

6464 put (args ++ [(x, n)])

6565 sc' <- unifyEq xs sc

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

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

6767 unifyEq xs t = do args <- get

6868 put (args ++ (zip xs (repeat (sUN "_"))))

6969 return t

@@ -73,13 +73,14 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

7373mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

7474mkPE_TyDecl ist args ty = mkty args ty

7575 where

76− mkty ((ExplicitD, v) : xs) (Bind n (Pi t) sc)

76+ mkty ((ExplicitD, v) : xs) (Bind n (Pi t k) sc)

7777 = 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)

7979 | concreteClass ist t = mkty xs sc

8080 | classConstraint ist t

8181 = PPi constraint n (delab ist t) (mkty xs sc)

8282 | otherwise = PPi impl n (delab ist t) (mkty xs sc)

83+

8384 mkty (_ : xs) t

8485 = mkty xs t

8586 mkty [] t = delab ist t

src/Idris/Primitives.hs+1−1

@@ -26,7 +26,7 @@ data Prim = Prim { p_name :: Name,

2626

2727ty :: [Const] -> Const -> Type

2828ty [] 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 (-3)))) (ty ts x)

3030

3131total, partial, iopartial :: Totality

3232total = Total []

src/Idris/REPL.hs+1−1

@@ -401,7 +401,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.Metavariables cols) =

401401 -- | Split a function type into a pair of premises, conclusion.

402402 -- Each maintains both the original and delaborated versions.

403403 splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

404− splitPi ist (Bind n (Pi t) rest) =

404+ splitPi ist (Bind n (Pi t _) rest) =

405405 let (hs, c, pc) = splitPi ist rest in

406406 ((n, t, delabTy' ist [] t False False):hs,

407407 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

112112 (numArgs, args, removedArgs, retTy) = go 0 [] [] t

113113

114114 -- 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

116116 if removePred t

117117 then go k args (arg : removedArgs) sc

118118 else go (succ k) (arg : args) removedArgs sc

@@ -346,7 +346,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

346346 unifyQueue state [] = return state

347347 unifyQueue state ((ty1, ty2) : queue) = do

348348 --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) []

350350 (state', queueAdditions) <- resolveUnis res state

351351 guard $ scoreCriterion (score state')

352352 unifyQueue state' (queue ++ queueAdditions)

test/quasiquote001/expected+3−3

@@ -1,5 +1,5 @@

1−(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 6)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6))))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 6)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 6))))))

1+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 10))))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 10))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10))))))

22--------------

3−(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 110))) (TType (UVar 112))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 114))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 36))) (Bind (MN 0 "B") (Pi (TType (UVar 38))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 28))) (Bind (MN 1 "B") (Pi (TType (UVar 30))) (TType (UVar 32))))) (V 3)) (V 2))))))) (TType (UVar 108))) (TType (UVar 110))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 116)))))

3+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 190))) (TType (UVar 192))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 194))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 196)))))

44--------------

5−(App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 36))) (Bind (MN 0 "B") (Pi (TType (UVar 38))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 28))) (Bind (MN 1 "B") (Pi (TType (UVar 30))) (TType (UVar 32))))) (V 3)) (V 2))))))) (TType (UVar 108))) (TType (UVar 110))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 36))) (Bind (MN 0 "B") (Pi (TType (UVar 38))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 28))) (Bind (MN 1 "B") (Pi (TType (UVar 30))) (TType (UVar 32))))) (V 3)) (V 2))))))) (TType (UVar 108))) (TType (UVar 110))) (TType (UVar 110))) (TType (UVar 110)))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 36))) (Bind (MN 0 "B") (Pi (TType (UVar 38))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 28))) (Bind (MN 1 "B") (Pi (TType (UVar 30))) (TType (UVar 32))))) (V 3)) (V 2))))))) (TType (UVar 108))) (TType (UVar 110))) (TType (UVar 110))) (TType (UVar 110))))

5+(App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (TType (UVar 190))) (TType (UVar 190)))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (TType (UVar 190))) (TType (UVar 190))))

test/unique001/expected+13−1

@@ -1,7 +1,19 @@

1119,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END

2219,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END

3338,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

4−unique001a.idr:23:11:Unique name xs is used more than once

4+38,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

5+unique001a.idr:33:11:Can't convert

6+ [94mInt[0m -> [94mString[0m

7+with

8+ UniqueType ([94mInt[0m -> [94mString[0m)

9+unique001a.idr:44:12:Can't convert

10+ [94mInt[0m -> [94mString[0m

11+with

12+ UniqueType ([94mInt[0m -> [94mString[0m)

13+unique001a.idr:55:12:Can't convert

14+ UniqueType ([94mInt[0m -> [94mString[0m)

15+with

16+ [94mInt[0m -> [94mString[0m

517unique001b.idr:16:7:Borrowed name xs must not be used on RHS

618unique001c.idr:49:6:Unique name f is used more than once

719unique001d.idr:3:7:Borrowed name x must not be used on RHS

test/unique001/unique001.idr+1

@@ -25,6 +25,7 @@ showStuff xs = do

2525 putStrLn (showU xs)

2626 let xs' = umap (*2) xs

2727 putStrLn (showU xs')

28+ putStrLn (showU xs')

2829

2930main : IO ()

3031main = showStuff (mkUList 20)

test/unique001/unique001a.idr+35−4

@@ -19,13 +19,44 @@ mkUList : Nat -> UList Int

1919mkUList Z = []

2020mkUList (S k) = cast k :: mkUList k

2121

22+showIt : UList Int -> Int -> String

23+showIt xs x = let xs' = umap (*2) xs in ""

24+

25+printThings : (Int -> String) -> IO ()

26+printThings f = do putStrLn (f 10)

27+ putStrLn (f 20)

28+

29+double : Int -> Int

30+double x = x * 2

31+

2232showStuff : UList Int -> IO ()

2333showStuff xs = do

2434 putStrLn (showU xs)

25− let xs' = umap (*2) xs

2635 putStrLn (showU xs)

27− putStrLn (showU xs')

36+ -- xsFn gets a unique type since we're in a unique context

37+ -- now, but function built has a non-unique type

38+ (\xsFn : Int -> String =>

39+ do putStrLn "Hello"

40+ putStrLn (xsFn 42))

41+ (\dummy => showU (umap double xs))

42+

43+showStuff' : UList Int -> IO ()

44+showStuff' xs = do

45+ putStrLn (showU xs)

46+ putStrLn (showU xs)

47+ -- xsFn gets a unique type since we're in a unique context

48+ -- now, but function built has a non-unique type

49+ let xsFn = \dummy : Int => showU (umap double xs)

50+ putStrLn "Hello"

51+ putStrLn (xsFn 42)

52+ putStrLn (xsFn 42)

53+

54+showThings : UList Int -> IO ()

55+showThings xs = do

56+ putStrLn (showU xs)

57+ putStrLn (showU xs)

58+ -- showIt has a unique type, printThings wants a non-unique

59+ -- type

60+ printThings (showIt xs)

2861

29−main : IO ()

30−main = showStuff (mkUList 20)

3162

test/unique002/expectednew file+5

@@ -0,0 +1,5 @@

1+unique002.idr:15:5:Unique name xs is used more than once

2+unique002a.idr:15:5:Can't convert

3+ [94mInt[0m -> [94mString[0m

4+with

5+ UniqueType ([94mInt[0m -> [94mString[0m)

test/unique002/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ unique002.idr --check

3+idris $@ unique002a.idr --check

4+rm -f *.ibc

test/unique002/unique002.idrnew file+20

@@ -0,0 +1,20 @@

1+data UList : Type -> UniqueType where

2+ Nil : UList a

3+ (::) : a -> UList a -> UList a

4+

5+free : {a : UniqueType} -> a -> String

6+free xs = ""

7+

8+showU : Show a => Borrowed (UList a) -> String

9+showU xs = "[" ++ showU' xs ++ "]" where

10+ showU' : Borrowed (UList a) -> String

11+ showU' [] = ""

12+ showU' (x :: xs) = show x ++ ", " ++ showU xs

13+

14+foo : UList Int -> IO ()

15+foo xs = do -- let f = \x : Int => showU xs

16+ putStrLn $ free xs

17+ putStrLn $ f 42

18+ return ()

19+ where f : Int -> String

20+ f x = showU xs

test/unique002/unique002a.idrnew file+18

@@ -0,0 +1,18 @@

1+data UList : Type -> UniqueType where

2+ Nil : UList a

3+ (::) : a -> UList a -> UList a

4+

5+free : {a : UniqueType} -> a -> String

6+free xs = ""

7+

8+showU : Show a => Borrowed (UList a) -> String

9+showU xs = "[" ++ showU' xs ++ "]" where

10+ showU' : Borrowed (UList a) -> String

11+ showU' [] = ""

12+ showU' (x :: xs) = show x ++ ", " ++ showU xs

13+

14+foo : UList Int -> IO ()

15+foo xs = do let f = \x : Int => showU xs

16+ putStrLn $ free xs

17+ putStrLn $ f 42

18+ return ()

test/unique003/expectednew file+4

@@ -0,0 +1,4 @@

1+unique003.idr:18:5:Can't convert

2+ [94mInt[0m -> [94mString[0m

3+with

4+ UniqueType ([94mInt[0m -> [94mString[0m)

test/unique003/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ unique003.idr --check

3+rm -f *.ibc

test/unique003/unique003.idrnew file+22

@@ -0,0 +1,22 @@

1+module Main

2+

3+data UList : Type -> UniqueType where

4+ Nil : UList a

5+ (::) : a -> UList a -> UList a

6+

7+showU : Show a => Borrowed (UList a) -> String

8+showU xs = "[" ++ showU' xs ++ "]" where

9+ showU' : Borrowed (UList a) -> String

10+ showU' [] = ""

11+ showU' [x] = show x

12+ showU' (x :: xs) = show x ++ ", " ++ showU' xs

13+

14+free : {a : UniqueType} -> a -> String

15+free xs = ""

16+

17+foo : UList Int -> IO ()

18+foo xs = do let f = \x : Int => showU xs -- can't build this in unique context

19+ putStrLn (f 10)

20+ putStrLn $ free xs

21+ putStrLn (f 10)

22+ return ()