17fe233 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+10−9

compare with master

unifiedsplit

@@ -1124,10 +1124,10 @@ addStatics n tm ptm =

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

1125 addIBC (IBCStatic n)

1126 where

1127− initStatics (Bind n (Pi ty _) sc) (PPi p n' t s)

1127+ initStatics (Bind n (Pi _ ty _) sc) (PPi p n' t s)

1128 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' t s) in

1129 (static, (n, ty) : dynamic)

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

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

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

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

1133 else if (not (searchArg p))

@@ -1143,16 +1143,16 @@ addStatics n tm ptm =

1143 getNamePos i ps (P _ n _ : as)

1144 | i `elem` ps = n : getNamePos (i + 1) ps as

1145 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as

1146− getParamNames ist (Bind t (Pi (P _ n _) _) sc)

1146+ getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)

1147 = n : getParamNames ist sc

1148 getParamNames ist _ = []

1149

1150− getNamesFrom i ps (Bind n (Pi _ _) sc)

1150+ getNamesFrom i ps (Bind n (Pi _ _ _) sc)

1151 | i `elem` ps = n : getNamesFrom (i + 1) ps sc

1152 | otherwise = getNamesFrom (i + 1) ps sc

1153 getNamesFrom i ps sc = []

1154

1155− freeArgNames (Bind n (Pi ty _) sc)

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

1156 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here

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

1158 concatMap freeNames args

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

1164 searchArg (TacImp _ _ _) = True

1165 searchArg _ = False

1166

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

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

1168 staticList _ _ = []

1169

1170-- Dealing with implicit arguments

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

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

1266 collectImps _ = []

1267

1268− getImps (Bind n (Pi t _) sc) imps

1268+ getImps (Bind n (Pi True _ _) sc) imps = getImps sc imps

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

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

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

1270 where

1271 where

1271 argInfo n (Imp opt _ _) t'

1272 argInfo n (Imp opt _ _) t'

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

1279 argInfo n (TacImp opt _ scr) t'

1280 argInfo n (TacImp opt _ scr) t'

1280 = (InaccessibleArg `elem` opt,

1281 = (InaccessibleArg `elem` opt,

1281 PTacImplicit 10 opt n scr t')

1282 PTacImplicit 10 opt n scr t')

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

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

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

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

1284 getImps sc tm = []

1285 getImps sc tm = []

1285

1286

@@ -1711,7 +1712,7 @@ stripUnmatchable :: IState -> PTerm -> PTerm

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

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

1712 su :: PTerm -> PTerm

1713 su :: PTerm -> PTerm

1713 su (PRef fc f)

1714 su (PRef fc f)

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

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

1715 = Placeholder

1716 = Placeholder

1716 su (PApp fc f@(PRef _ fn) args)

1717 su (PApp fc f@(PRef _ fn) args)

1717 | isDConName fn ctxt

1718 | isDConName fn ctxt

src/Idris/AbsSyntaxTree.hs+1−1

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

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

1141

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

1143− where toTy (Lam t) = Pi t (TType (UVar 0))

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

1144 toTy (PVar t) = PVTy t

1145 toTy b = b

1146getInferType (App (App _ ty) _) = ty

src/Idris/Apropos.hs+1−1

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

66

67instance Apropos (Binder (TT Name)) where

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

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

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

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

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

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

src/Idris/CaseSplit.hs+1−1

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

183 = case lookupTy n (tt_ctxt ist) of

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

185 _ -> repeat Nothing

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

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

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

188 | otherwise = Nothing

189argTys _ _ = repeat Nothing

src/Idris/Core/Binary.hs+6−4

@@ -409,9 +409,10 @@ instance (Binary b) => Binary (Binder b) where

409 = case x of

410 Lam x1 -> do putWord8 0

411 put x1

412− Pi x1 x2 -> do putWord8 1

412+ Pi x1 x2 x3 -> do putWord8 1

413− put x1

413+ put x1

414− put x2

414+ put x2

415+ put x3

415 Let x1 x2 -> do putWord8 2

416 Let x1 x2 -> do putWord8 2

416 put x1

417 put x1

417 put x2

418 put x2

@@ -437,7 +438,8 @@ instance (Binary b) => Binary (Binder b) where

437 return (Lam x1)

438 return (Lam x1)

438 1 -> do x1 <- get

439 1 -> do x1 <- get

439 x2 <- get

440 x2 <- get

441+ x3 <- get

440− return (Pi x1 x2)

442+ return (Pi x1 x2 x3)

441 2 -> do x1 <- get

443 2 -> do x1 <- get

442 x2 <- get

444 x2 <- get

443 return (Let x1 x2)

445 return (Let x1 x2)

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

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

370 toPat' [] (Constant x) | isTypeConst x = PTyPat

371 | otherwise = 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

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

91

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

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

94− rnf (Pi x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

94+ rnf (Pi x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

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

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

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

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

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

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

269 isInj ctxt (Constant _) = True

270 isInj ctxt (TType _) = True

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

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

272 isInj ctxt _ = False

273

274-- get instance argument names

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

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

507 -> [Name] -- ^ Hypotheses

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

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

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

510 do let t = rebind hs t_in

511 n <- getNameFrom (mkMN n')

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

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

614 priOrder _ Nothing = GT

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

616

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

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

618 do n <- unique_hole (mkMN n')

619 when (null claims) (start_unify n)

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

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

649checkPiGoal n

650 = do g <- goal

651 case g of

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

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

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

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

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

656 claim a RType

657 claim b RType

658− claim f (RBind n (Pi (Var a) RType) (Var b))

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

659 movelast a

660 movelast b

661 fill (Var f)

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

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

671 claim a RType

672 claim b RType

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

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

674 tm <- get_term

675 start_unify s

676 claim s (Var a)

src/Idris/Core/Evaluate.hs+2−2

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

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

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

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

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

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

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

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

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

@@ -602,7 +602,7 @@ convEq ctxt holes topx topy = ceq [] topx topy where

602 where

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

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

605− ceqB ps (Pi v t) (Pi v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

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

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

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

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

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

@@ -88,7 +88,7 @@ toTT (EBind n b body) = do n' <- newN n

88 b' <- fixBinder b

89 Bind n' b' <$> toTT body'

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

91− fixBinder (Pi t k) = Pi <$> toTT t <*> toTT k

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

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

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

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

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

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

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

413 where

414 mkTy [] t = t

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

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

416

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

418

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

540 Just name -> name

541 Nothing -> x

542 let t' = case t of

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

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

544 _ -> hnf ctxt env t

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

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

547 case t' of

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

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

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

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

550− ps <- get

550+ ps <- get

551− let (uh, uns) = unified ps

551+ let (uh, uns) = unified ps

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

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

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

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

554 _ -> lift $ tfail $ CantIntroduce t'

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

556

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

560 Just name -> name

561 Nothing -> x

562 let t' = case t of

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

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

564 _ -> hnf ctxt env t

565 case t' of

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

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

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

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

569 _ -> lift $ tfail $ CantIntroduce t'

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

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

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

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

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

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

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

579

580patvar :: Name -> RunTactic

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

@@ -679,9 +679,13 @@ deriving instance NFData Raw

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

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

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

682+ | Pi { binderImpl :: Bool,

682− | Pi { binderTy :: !b,

683+ binderTy :: !b,

683 binderKind :: !b }

684 binderKind :: !b }

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

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

686+ The 'binderImpl' flag says whether it was a scoped implicit

687+ (i.e. forall bound) in the high level Idris, but otherwise

688+ has no relevance in TT. -}

685 | Let { binderTy :: !b,

689 | Let { binderTy :: !b,

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

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

687 -- ^ A binding that occurs in a @let@ expression

691 -- ^ A binding that occurs in a @let@ expression

@@ -703,7 +707,7 @@ deriving instance NFData Binder

703

707

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

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

705 size (Lam ty) = 1 + size ty

709 size (Lam ty) = 1 + size ty

706− size (Pi ty _) = 1 + size ty

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

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

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

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

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

709 size (Hole ty) = 1 + size ty

713 size (Hole ty) = 1 + size ty

@@ -717,7 +721,7 @@ fmapMB f (Let t v) = liftM2 Let (f t) (f v)

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

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

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

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

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

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

720−fmapMB f (Pi t k) = liftM2 Pi (f t) (f k)

724+fmapMB f (Pi i t k) = liftM2 (Pi i) (f t) (f k)

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

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

722fmapMB f (GHole i t) = liftM (GHole i) (f t)

726fmapMB f (GHole i t) = liftM (GHole i) (f t)

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

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

@@ -884,7 +888,7 @@ isInjective (P (DCon _ _ _) _ _) = True

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

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

885isInjective (Constant _) = True

889isInjective (Constant _) = True

886isInjective (TType x) = True

890isInjective (TType x) = True

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

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

888isInjective (App f a) = isInjective f

892isInjective (App f a) = isInjective f

889isInjective _ = False

893isInjective _ = False

890

894

@@ -1099,7 +1103,7 @@ freeNames t = nub $ freeNames' t

1099

1103

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

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

1101arity :: TT n -> Int

1105arity :: TT n -> Int

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

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

1103arity _ = 0

1107arity _ = 0

1104

1108

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

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

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

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

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

1160getArgTys (Bind n (PVar _) sc) = getArgTys sc

1164getArgTys (Bind n (PVar _) sc) = getArgTys sc

1161getArgTys (Bind n (PVTy _) sc) = getArgTys sc

1165getArgTys (Bind n (PVTy _) sc) = getArgTys sc

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

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

1163getArgTys _ = []

1167getArgTys _ = []

1164

1168

1165getRetTy :: TT n -> TT n

1169getRetTy :: TT n -> TT n

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

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

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

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

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

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

1169getRetTy sc = sc

1173getRetTy sc = sc

1170

1174

1171uniqueNameFrom :: [Name] -> [Name] -> Name

1175uniqueNameFrom :: [Name] -> [Name] -> Name

@@ -1281,7 +1285,7 @@ prettyEnv env t = prettyEnv' env t False

1281 else

1285 else

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

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

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

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

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

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

1285 | noOccurrence n sc && not debug =

1289 | noOccurrence n sc && not debug =

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

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

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

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

@@ -1297,7 +1301,7 @@ prettyEnv env t = prettyEnv' env t False

1297 -- Render a `Binder` and its name

1301 -- Render a `Binder` and its name

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1323,7 +1327,7 @@ showEnv' env t dbg = se 10 env t where

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

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

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

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

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

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

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

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

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

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

1328 where arrow (TType _) = " -> "

1332 where arrow (TType _) = " -> "

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

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

@@ -1339,7 +1343,7 @@ showEnv' env t dbg = se 10 env t where

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1399,7 +1403,7 @@ orderPats tm = op [] tm

1399

1403

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

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

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

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

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

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

1403 op ps sc = bindAll (sortP ps) sc

1407 op ps sc = bindAll (sortP ps) sc

1404

1408

1405 sortP ps = pick [] (reverse ps)

1409 sortP ps = pick [] (reverse ps)

@@ -1445,10 +1449,10 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in

1445 v' <- getPats v

1449 v' <- getPats v

1446 sc' <- getPats sc

1450 sc' <- getPats sc

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

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

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

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

1449− k' <- getPats k

1453+ k' <- getPats k

1450− sc' <- getPats sc

1454+ sc' <- getPats sc

1451− return (Bind n (Pi t' k') sc')

1455+ return (Bind n (Pi i t' k') sc')

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

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

1453 sc' <- getPats sc

1457 sc' <- getPats sc

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

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

src/Idris/Core/Typecheck.hs+13−13

@@ -87,13 +87,13 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

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

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

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

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

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

91 _ -> uniqueBinders (map fst env)

92 $ case hnf ctxt env fty of

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

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

94 _ -> normalise ctxt env fty

95 case fty' of

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

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

97 do convertsC ctxt env aty s

98 let apty = simplify initContext env

99 (Bind x (Let aty av) t)

@@ -133,25 +133,25 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

133 constType _ = TType (UVal 0)

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

135 return (Erased, ty)

136− chk u env (RBind n (Pi s k) t)

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

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

138 (kv, kt) <- chk u env k

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

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

140 (v, cs) <- get

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

142 (TType su, TType tu) -> do

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

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

145− return (Bind n (Pi (uniqueBinders (map fst env) sv) k')

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

146 (pToV n tv), k')

147 (un, un') ->

148 let k' = st `smaller` kv `smaller` un `smaller` un' `smaller` u in

149− return (Bind n (Pi (uniqueBinders (map fst env) sv) k')

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

150 (pToV n tv), k')

151

152− where mkUniquePi kv (Bind n (Pi s k) sc)

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

153 = let k' = smaller kv k in

154− Bind n (Pi s k') (mkUniquePi k' sc)

154+ Bind n (Pi i s k') (mkUniquePi k' sc)

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

156 = Bind n (Lam (mkUniquePi kv t)) (mkUniquePi kv sc)

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

@@ -161,7 +161,7 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

161 -- Kind of the whole thing is the kind of the most unique thing

162 -- in the environment (because uniqueness taints everything...)

163 mostUnique [] k = k

164− mostUnique (Pi _ pk : es) k = mostUnique es (smaller pk k)

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

165 mostUnique (_ : es) k = mostUnique es k

166

167 chk u env (RBind n b sc)

@@ -230,9 +230,9 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

230 return (PVTy tv, tt')

231

232 discharge n (Lam t) bt scv sct

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

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

234− discharge n (Pi t k) bt scv sct

234+ discharge n (Pi i t k) bt scv sct

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

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

236 discharge n (Let t v) bt scv sct

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

238 discharge n (NLet t v) bt scv sct

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

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

94 StateT UInfo

95 TC [(Name, TT Name)]

96

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

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

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

99 holeIn env f || f `elem` holes

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

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

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

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

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

104 holeIn env f || f `elem` holes

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

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

143 h2 <- un bnames vx vy

144 combine bnames h1 h2

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

146− uB bnames (Pi tx _) (Pi ty _) = un bnames tx ty

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

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

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

149 (normalise ctxt env (binderTy y))

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

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

432 -- class resolution for type classes over functions.

433

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

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

435 | noOccurrence n y && injectiveApp f

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

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

438− (Bind n (Pi t k) (V 1)))

438+ (Bind n (Pi i t k) (V 1)))

439 combine bnames ux uf

440

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

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

442 | noOccurrence n y && injectiveApp f

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

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

445− (Bind n (Pi t k) (V 1))) f

445+ (Bind n (Pi i t k) (V 1))) f

446 combine bnames ux uf

447

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

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

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

452 combine bnames h1 h2

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

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

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

455 sameBinder _ _ = False

456 un' fn bnames x y

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

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

583 sc 1

584 combine bnames h1 h2

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

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

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

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

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

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

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

686 | f == f' = recoverable a a'

687recoverable (App f a) (App f' a')

688 = recoverable f f' -- && recoverable a a'

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

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

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

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

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

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

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

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

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

src/Idris/Coverage.hs+4−4

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

286 where

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

288

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

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

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

291 n' `elem` mut_ns = all noRec args

292 cp _ = True

293

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

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

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

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

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

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

536 = case lookupTy n (tt_ctxt ist) of

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

538 _ -> args

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

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

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

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

541 expand i _ xs = xs

542

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

src/Idris/Delaborate.hs+7−7

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

57 _ -> PRef un n

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

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

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

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

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

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

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

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

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

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

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

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

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

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

68 n

69 (de env [] ty)

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

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

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

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

73

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

@@ -222,9 +222,9 @@ pprintErr' i (CantConvert x_in y_in env) =

222 indented (annTm y_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

223 y)) <>

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

225− where flagUnique (Bind n (Pi t k@(UType u)) sc)

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

226 = App (P Ref (sUN (show u)) Erased)

227− (Bind n (Pi (flagUnique t) k) (flagUnique sc))

227+ (Bind n (Pi i (flagUnique t) k) (flagUnique sc))

228 flagUnique (App f a) = App (flagUnique f) (flagUnique a)

229 flagUnique (Bind n b sc) = Bind n (fmap flagUnique b) (flagUnique sc)

230 flagUnique t = t

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

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

867 let wargval = getRetTy cwvalN

868 let wargtype = getRetTy cwvaltyN

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

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

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

871 (sMN 0 "warg", wargtype) :

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

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

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

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

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

925 where

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

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

927 getImps _ = []

928

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

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

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

177 getDataApp f@(App _ _)

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

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

180− getDataApp (Bind n (Pi t _) sc)

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

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

182 getDataApp _ = []

183

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

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

104

105 return (cty, ckind, ty, inacc)

106 where

107− patToImp (Bind n (PVar t) sc) = Bind n (Pi t (TType (UVar 0))) (patToImp sc)

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

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

109 patToImp t = t

110

111− param_pos i ns (Bind n (Pi t _) sc)

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

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

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

114 param_pos i ns t = []

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

196 lst = txt "List"

197 errrep = txt "ErrorReportPart"

198

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

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

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

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

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

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

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

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

50-- type

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

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

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

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

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

55inaccessibleImps _ _ _ = []

@@ -155,13 +155,13 @@ psolve tm = return ()

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

156pvars ist _ = []

157

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

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

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

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

161 ++ case t of

162 P _ n _ -> if n `elem` env then [n] else []

163 _ -> []

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

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

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

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

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

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

175 getFixedInType i env is a

176getFixedInType i _ _ _ = []

177

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

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

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

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

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

@@ -256,7 +256,7 @@ getStaticNames ist tm

256getStaticNames _ _ = []

257

258getStatics :: [Name] -> Term -> [Bool]

259−getStatics ns (Bind n (Pi _ _) t)

259+getStatics ns (Bind n (Pi _ _ _) t)

260 | n `elem` ns = True : getStatics ns t

261 | otherwise = False : getStatics ns t

262getStatics _ _ = []

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))) (TType (UVar (-1))))

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

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

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

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

108+ (Bind (sUN "x") (Pi False (V 1) (TType (UVar (-1)))) (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))) (TType (UVar (-2))))

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

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

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

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

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

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

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

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

@@ -152,7 +152,7 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon

152 Nothing -> []

153 Just ty -> checkArgs [] [] ty

154 where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]

155− checkArgs env ns (Bind n (Pi t _) sc)

155+ checkArgs env ns (Bind n (Pi _ t _) sc)

156 = let env' = case t of

157 TType _ -> n : env

158 _ -> env in

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

564 ans <- claimArgTys env xs

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

566 fnTy [] ret = forget ret

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

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

568

569 localVar env (PRef _ x)

570 = case lookup x env of

@@ -1516,9 +1516,9 @@ runTac autoSolve ist perhapsFC fn tac

1516 where tacticTy = Var (reflm "Tactic")

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

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

1519− (Pi (RApp listTy envTupleType) RType)

1519+ (Pi False (RApp listTy envTupleType) RType)

1520 (RBind (sMN 1 "__pi_arg")

1521− (Pi (Var $ reflm "TT") RType) tacticTy))

1521+ (Pi False (Var $ reflm "TT") RType) tacticTy))

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

1523 -- goal, then apply the resulting reflected Tactic

1524 = do tgoal <- goal

@@ -1791,7 +1791,7 @@ reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)

1791reifyTTBinderApp reif f [t]

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

1793reifyTTBinderApp reif f [t, k]

1794− | f == reflm "Pi" = liftM2 Pi (reif t) (reif k)

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

1795reifyTTBinderApp reif f [x, y]

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

1797reifyTTBinderApp reif f [x, y]

@@ -1934,7 +1934,7 @@ reflectQuotePattern unq (Bind n b x)

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

1935 solve

1936 focus t'; reflectQuotePattern unq t

1937− reflectBinderQuotePattern unq (Pi t k)

1937+ reflectBinderQuotePattern unq (Pi _ t k)

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

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

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

@@ -2084,7 +2084,7 @@ reflectBinder = reflectBinderQuote []

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

2085reflectBinderQuote unq (Lam t)

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

2087−reflectBinderQuote unq (Pi t k)

2087+reflectBinderQuote unq (Pi _ t k)

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

2089reflectBinderQuote unq (Let x y)

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

src/Idris/Erasure.hs+1−1

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

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

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

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

357− | Pi ty _ <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd body

357+ | Pi _ ty _ <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd body

358

359 -- let-bound variables can get partially evaluated

360 -- it is sufficient just to plug the Cond in when the bound names are used

src/Idris/IBC.hs+1−1

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

35import Util.Zlib (decompressEither)

36

37ibcVersion :: Word8

38−ibcVersion = 92

38+ibcVersion = 93

39

40data IBCFile = IBCFile { ver :: Word8,

41 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+12−12

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

85 where

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

87 -- of expecting it as a function argument

88− st ((ExplicitS, v) : xs) (Bind n (Pi t _) sc)

88+ st ((ExplicitS, v) : xs) (Bind n (Pi _ t _) sc)

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

90− st ((ImplicitS, v) : xs) (Bind n (Pi t _) sc)

90+ st ((ImplicitS, v) : xs) (Bind n (Pi _ t _) sc)

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

92 -- Erase argument from function type

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

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

94 = st xs sc

95 -- Keep types as is

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

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

97− = Bind n (Pi t k) (st xs sc)

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

98 st _ t = t

99

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

101 -- by substituting the value of previous argument

102− unifyEq (imp@(ImplicitD, v) : xs) (Bind n (Pi t k) sc)

102+ unifyEq (imp@(ImplicitD, v) : xs) (Bind n (Pi i t k) sc)

103 = do amap <- get

104 case lookup imp amap of

105 Just n' ->

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

107 sc' <- unifyEq xs (subst n (P Bound n' Erased) sc)

108− return (Bind n (Pi t k) sc') -- erase later

108+ return (Bind n (Pi i t k) sc') -- erase later

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

110 sc' <- unifyEq xs sc

111− return (Bind n (Pi t k) sc')

111+ return (Bind n (Pi i t k) sc')

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

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

113 = do args <- get

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

115 sc' <- unifyEq xs sc

116− return (Bind n (Pi t k) sc')

116+ return (Bind n (Pi i t k) sc')

117 unifyEq xs t = do args <- get

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

119 return t

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

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

128mkPE_TyDecl ist args ty = mkty args ty

129 where

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

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

131 = PPi expl n (delab ist (generaliseIn t)) (mkty xs sc)

132− mkty ((ImplicitD, v) : xs) (Bind n (Pi t k) sc)

132+ mkty ((ImplicitD, v) : xs) (Bind n (Pi _ t k) sc)

133 | concreteClass ist t = mkty xs sc

134 | classConstraint ist t

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

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) (TType (UVar (-3)))) (ty ts x)

29+ty (t:ts) x = Bind (sMN 0 "T") (Pi False (Constant t) (TType (UVar (-3)))) (ty ts x)

30

31total, partial, iopartial :: Totality

32total = Total []

src/Idris/REPL.hs+1−1

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

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

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

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

405− splitPi ist (Bind n (Pi t _) rest) =

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

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

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

408 c, delabTy' ist [] c False False)

src/Idris/TypeSearch.hs+2−2

@@ -120,7 +120,7 @@ computeDagP removePred t = (reverse (map f arguments), reverse theRemovedArgs ,

120 (arguments, theRemovedArgs, retTy) = go [] [] t

121

122 -- NOTE : args are in reverse order

123− go args removedArgs (Bind n (Pi ty _) sc) = let arg = (n, ty) in

123+ go args removedArgs (Bind n (Pi _ ty _) sc) = let arg = (n, ty) in

124 if removePred ty

125 then go args (arg : removedArgs) sc

126 else go (arg : args) removedArgs sc

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

416 unifyQueue state [] = return state

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

418 --trace ("go: \n" ++ show state) True `seq` return ()

419− res <- tcToMaybe $ match_unify ctxt [ (n, Pi ty (TType (UVar 0))) | (n, ty) <- holes state] ty1 ty2 [] (map fst $ holes state) []

419+ res <- tcToMaybe $ match_unify ctxt [ (n, Pi False ty (TType (UVar 0))) | (n, ty) <- holes state] ty1 ty2 [] (map fst $ holes state) []

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

421 guard $ scoreCriterion (score state')

422 unifyQueue state' (queue ++ queueAdditions)