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

src/Idris/AbsSyntax.hs+10−9

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

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

11251125 addIBC (IBCStatic n)

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

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

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

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

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

11331133 else if (not (searchArg p))

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

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

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

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

11471147 = n : getParamNames ist sc

11481148 getParamNames ist _ = []

11491149

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

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

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

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

11531153 getNamesFrom i ps sc = []

11541154

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

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

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

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

11581158 concatMap freeNames args

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

11641164 searchArg (TacImp _ _ _) = True

11651165 searchArg _ = False

11661166

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

11681168 staticList _ _ = []

11691169

11701170-- Dealing with implicit arguments

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

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

12661266 collectImps _ = []

12671267

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

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

12701271 where

12711272 argInfo n (Imp opt _ _) t'

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

12791280 argInfo n (TacImp opt _ scr) t'

12801281 = (InaccessibleArg `elem` opt,

12811282 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

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

12841285 getImps sc tm = []

12851286

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

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

17121713 su :: PTerm -> PTerm

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

17151716 = Placeholder

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

17171718 | isDConName fn ctxt

src/Idris/AbsSyntaxTree.hs+1−1

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

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

11411141

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

11441144 toTy (PVar t) = PVTy t

11451145 toTy b = b

11461146getInferType (App (App _ ty) _) = ty

src/Idris/Apropos.hs+1−1

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

6666

6767instance Apropos (Binder (TT Name)) where

6868 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

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

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

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

183183 = case lookupTy n (tt_ctxt ist) of

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

185185 _ -> repeat Nothing

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

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

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

188188 | otherwise = Nothing

189189argTys _ _ = repeat Nothing

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

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

409409 = case x of

410410 Lam x1 -> do putWord8 0

411411 put x1

412− Pi x1 x2 -> do putWord8 1

413− put x1

414− put x2

412+ Pi x1 x2 x3 -> do putWord8 1

413+ put x1

414+ put x2

415+ put x3

415416 Let x1 x2 -> do putWord8 2

416417 put x1

417418 put x2

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

437438 return (Lam x1)

438439 1 -> do x1 <- get

439440 x2 <- get

440− return (Pi x1 x2)

441+ x3 <- get

442+ return (Pi x1 x2 x3)

441443 2 -> do x1 <- get

442444 x2 <- get

443445 return (Let x1 x2)

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

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

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

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

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

9191

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

9393 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` ()

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

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

9797 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

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

269269 isInj ctxt (Constant _) = True

270270 isInj ctxt (TType _) = True

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

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

272272 isInj ctxt _ = False

273273

274274-- get instance argument names

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

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

507507 -> [Name] -- ^ Hypotheses

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

510510 do let t = rebind hs t_in

511511 n <- getNameFrom (mkMN n')

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

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

614614 priOrder _ Nothing = GT

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

616616

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

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

618618 do n <- unique_hole (mkMN n')

619619 when (null claims) (start_unify n)

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

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

649649checkPiGoal n

650650 = do g <- goal

651651 case g of

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

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

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

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

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

656656 claim a RType

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

659659 movelast a

660660 movelast b

661661 fill (Var f)

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

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

671671 claim a RType

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

674674 tm <- get_term

675675 start_unify s

676676 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

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

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

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

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

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

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

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

602602 where

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

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

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

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

608608 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

8888 b' <- fixBinder b

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

9090 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

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

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

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

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

413413 where

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

416416

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

418418

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

540540 Just name -> name

541541 Nothing -> x

542542 let t' = case t of

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

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

544544 _ -> hnf ctxt env t

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

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

547547 case t' of

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

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

550− ps <- get

551− let (uh, uns) = unified ps

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

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

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

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

550+ ps <- get

551+ let (uh, uns) = unified ps

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

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

554554 _ -> lift $ tfail $ CantIntroduce t'

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

556556

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

560560 Just name -> name

561561 Nothing -> x

562562 let t' = case t of

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

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

564564 _ -> hnf ctxt env t

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

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

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

569569 _ -> lift $ tfail $ CantIntroduce t'

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

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

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

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

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

579579

580580patvar :: Name -> RunTactic

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

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

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

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

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

682− | Pi { binderTy :: !b,

682+ | Pi { binderImpl :: Bool,

683+ binderTy :: !b,

683684 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. -}

685689 | Let { binderTy :: !b,

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

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

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

703707

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

705709 size (Lam ty) = 1 + size ty

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

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

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

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

709713 size (Hole ty) = 1 + size ty

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

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

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

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

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

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

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

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

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

885889isInjective (Constant _) = True

886890isInjective (TType x) = True

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

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

888892isInjective (App f a) = isInjective f

889893isInjective _ = False

890894

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

10991103

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

11011105arity :: TT n -> Int

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

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

11031107arity _ = 0

11041108

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

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

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

11611165getArgTys (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

11631167getArgTys _ = []

11641168

11651169getRetTy :: TT n -> TT n

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

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

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

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

11691173getRetTy sc = sc

11701174

11711175uniqueNameFrom :: [Name] -> [Name] -> Name

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

12811285 else

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

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

12851289 | noOccurrence n sc && not debug =

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

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

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

12971301 -- Render a `Binder` and its name

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

12991303 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

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

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

13031307 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

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

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

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

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

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

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

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

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

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

13411345 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

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

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

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

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

13991403

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

14011405 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

14031407 op ps sc = bindAll (sortP ps) sc

14041408

14051409 sortP ps = pick [] (reverse ps)

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

14451449 v' <- getPats v

14461450 sc' <- getPats sc

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

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

1449− k' <- getPats k

1450− sc' <- getPats sc

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

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

1453+ k' <- getPats k

1454+ sc' <- getPats sc

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

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

14531457 sc' <- getPats sc

14541458 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

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

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

8989 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

9191 _ -> uniqueBinders (map fst env)

9292 $ 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

9494 _ -> normalise ctxt env fty

9595 case fty' of

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

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

9797 do convertsC ctxt env aty s

9898 let apty = simplify initContext env

9999 (Bind x (Let aty av) t)

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

133133 constType _ = TType (UVal 0)

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

135135 return (Erased, ty)

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

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

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

138138 (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

140140 (v, cs) <- get

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

142142 (TType su, TType tu) -> do

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

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

146146 (pToV n tv), k')

147147 (un, un') ->

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

150150 (pToV n tv), k')

151151

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

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

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

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

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

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

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

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

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

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

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

166166

167167 chk u env (RBind n b sc)

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

230230 return (PVTy tv, tt')

231231

232232 discharge n (Lam t) bt scv sct

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

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

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

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

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

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

236236 discharge n (Let t v) bt scv sct

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

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

9494 StateT UInfo

9595 TC [(Name, TT Name)]

9696

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)

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

9999 holeIn env f || f `elem` holes

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

101101 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

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

104104 holeIn env f || f `elem` holes

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

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

143143 h2 <- un bnames vx vy

144144 combine bnames h1 h2

145145 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

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

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

149149 (normalise ctxt env (binderTy y))

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

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

432432 -- class resolution for type classes over functions.

433433

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)

435435 | noOccurrence n y && injectiveApp f

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

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

439439 combine bnames ux uf

440440

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)

442442 | noOccurrence n y && injectiveApp f

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

444444 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

446446 combine bnames ux uf

447447

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

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

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

452452 combine bnames h1 h2

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

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

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

455455 sameBinder _ _ = False

456456 un' fn bnames x y

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

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

583583 sc 1

584584 combine bnames h1 h2

585585 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

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

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

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

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

686686 | f == f' = recoverable a a'

687687recoverable (App f a) (App f' a')

688688 = recoverable f f' -- && recoverable a a'

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

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

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

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

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

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

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

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

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

src/Idris/Coverage.hs+4−4

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

286286 where

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

288288

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

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

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

291291 n' `elem` mut_ns = all noRec args

292292 cp _ = True

293293

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

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

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

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

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

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

536536 = case lookupTy n (tt_ctxt ist) of

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

538538 _ -> args

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

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

541541 expand i _ xs = xs

542542

543543 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

5757 _ -> PRef un n

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

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

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

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

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

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

6868 n

6969 (de env [] ty)

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

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

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

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

7373

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

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

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

223223 y)) <>

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

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

228228 flagUnique (App f a) = App (flagUnique f) (flagUnique a)

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

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

867867 let wargval = getRetTy cwvalN

868868 let wargtype = getRetTy cwvaltyN

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

871871 (sMN 0 "warg", wargtype) :

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

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

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

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

925925 where

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

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

927927 getImps _ = []

928928

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

177177 getDataApp f@(App _ _)

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

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

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

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

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

182182 getDataApp _ = []

183183

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

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

104104

105105 return (cty, ckind, ty, inacc)

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

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

109109 patToImp t = t

110110

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

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

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

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

114114 param_pos i ns t = []

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

196196 lst = txt "List"

197197 errrep = txt "ErrorReportPart"

198198

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

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

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

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

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

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

5050-- type

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

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

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

5555inaccessibleImps _ _ _ = []

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

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

156156pvars ist _ = []

157157

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

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

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

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

161161 ++ case t of

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

163163 _ -> []

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

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

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

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

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

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

175175 getFixedInType i env is a

176176getFixedInType i _ _ _ = []

177177

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

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

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

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

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

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

256256getStaticNames _ _ = []

257257

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

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

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

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

261261 | otherwise = False : getStatics ns t

262262getStatics _ _ = []

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

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

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

108+ (Bind (sUN "x") (Pi False (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))) (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))))

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

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

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

132+ (Bind (sUN "y") (Pi False (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+7−7

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

152152 Nothing -> []

153153 Just ty -> checkArgs [] [] ty

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

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

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

156156 = let env' = case t of

157157 TType _ -> n : env

158158 _ -> env in

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

564564 ans <- claimArgTys env xs

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

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

568568

569569 localVar env (PRef _ x)

570570 = case lookup x env of

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

15161516 where tacticTy = Var (reflm "Tactic")

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

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

1519− (Pi (RApp listTy envTupleType) RType)

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

15201520 (RBind (sMN 1 "__pi_arg")

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

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

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

15231523 -- goal, then apply the resulting reflected Tactic

15241524 = do tgoal <- goal

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

17911791reifyTTBinderApp reif f [t]

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

17931793reifyTTBinderApp 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)

17951795reifyTTBinderApp reif f [x, y]

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

17971797reifyTTBinderApp reif f [x, y]

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

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

19351935 solve

19361936 focus t'; reflectQuotePattern unq t

1937− reflectBinderQuotePattern unq (Pi t k)

1937+ reflectBinderQuotePattern unq (Pi _ t k)

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

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

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

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

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

20852085reflectBinderQuote unq (Lam t)

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

2087−reflectBinderQuote unq (Pi t k)

2087+reflectBinderQuote unq (Pi _ t k)

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

20892089reflectBinderQuote unq (Let x y)

20902090 = 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]

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

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

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

358358

359359 -- let-bound variables can get partially evaluated

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

3535import Util.Zlib (decompressEither)

3636

3737ibcVersion :: Word8

38−ibcVersion = 92

38+ibcVersion = 93

3939

4040data IBCFile = IBCFile { ver :: Word8,

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

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

8585 where

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

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

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

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

9292 -- Erase argument from function type

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

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

9494 = st xs sc

9595 -- Keep types as is

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

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

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

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

9898 st _ t = t

9999

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

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

103103 = do amap <- get

104104 case lookup imp amap of

105105 Just n' ->

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

107107 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

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

110110 sc' <- unifyEq xs sc

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

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

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

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

113113 = do args <- get

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

115115 sc' <- unifyEq xs sc

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

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

117117 unifyEq xs t = do args <- get

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

119119 return t

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

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

128128mkPE_TyDecl ist args ty = mkty args ty

129129 where

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

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

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

133133 | concreteClass ist t = mkty xs sc

134134 | classConstraint ist t

135135 = 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,

2626

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

2828ty [] 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)

3030

3131total, partial, iopartial :: Totality

3232total = Total []

src/Idris/REPL.hs+1−1

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

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

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

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

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

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

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

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

408408 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 ,

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

121121

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

124124 if removePred ty

125125 then go args (arg : removedArgs) sc

126126 else go (arg : args) removedArgs sc

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

416416 unifyQueue state [] = return state

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

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

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

421421 guard $ scoreCriterion (score state')

422422 unifyQueue state' (queue ++ queueAdditions)