e1c210b · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+10−10

compare with master

unifiedsplit

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

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

1476 addIBC (IBCStatic n)

1477 where

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

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

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

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

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

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

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

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

1484 else if (not (searchArg p))

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

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

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

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

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

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

1498 = n : getParamNames ist sc

1499 getParamNames ist _ = []

1500

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

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

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

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

1504 getNamesFrom i ps sc = []

1505

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

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

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

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

1509 concatMap freeNames args

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

1515 searchArg (TacImp _ _ _) = True

1516 searchArg _ = False

1517

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

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

1519 staticList _ _ = []

1520

1521-- Dealing with implicit arguments

@@ -1623,9 +1623,9 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

1623 scopedimpl (Just i) = not (toplevel_imp i)

1624 scopedimpl _ = False

1625

1626− getImps (Bind n (Pi i _ _) sc) imps

1626+ getImps (Bind n (Pi _ i _ _) sc) imps

1627 | scopedimpl i = getImps sc imps

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

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

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

1630 where

1631 argInfo n (Imp opt _ _ _ _) Placeholder

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

1641 argInfo n (TacImp opt _ scr) t'

1642 = (InaccessibleArg `elem` opt,

1643 PTacImplicit 10 opt n scr t')

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

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

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

1646 getImps sc tm = []

1647

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

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

2147 su :: PTerm -> PTerm

2148 su tm@(PRef fc hl f)

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

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

2150 = Placeholder

2151 | (TType _ : _) <- lookupTy f (tt_ctxt i),

2152 not (implicitable f)

src/Idris/AbsSyntaxTree.hs+2−2

@@ -1619,8 +1619,8 @@ getInferTerm (App _ (App _ _ _) tm) = tm

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

1620

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

1622− where toTy (Lam t) = Pi Nothing t (TType (UVar [] 0))

1622+ where toTy (Lam t) = Pi RigW Nothing t (TType (UVar [] 0))

1623− toTy (PVar t) = PVTy t

1623+ toTy (PVar _ t) = PVTy t

1624 toTy b = b

1625getInferType (App _ (App _ _ ty) _) = ty

1626

src/Idris/Apropos.hs+1−1

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

73

74instance Apropos (Binder (TT Name)) where

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

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

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

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

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

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

src/Idris/CaseSplit.hs+1−1

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

212 [ty] -> let ty' = normalise (tt_ctxt ist) [] ty in

213 map (tyName . snd) (getArgTys ty') ++ repeat Nothing

214 _ -> repeat Nothing

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

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

216 tyName t | (P _ d _, [_, ty]) <- unApply t,

217 d == sUN "Delayed" = tyName ty

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

src/Idris/Core/Binary.hs+25−8

@@ -490,6 +490,19 @@ instance Binary Raw where

490 return (RUType x1)

491 _ -> error "Corrupted binary data for Raw"

492

493+instance Binary RigCount where

494+ put x = case x of

495+ Rig0 -> putWord8 0

496+ Rig1 -> putWord8 1

497+ RigW -> putWord8 2

498+ get = do i <- getWord8

499+ case i of

500+ 0 -> return Rig0

501+ 1 -> return Rig1

502+ 2 -> return RigW

503+ _ -> error "Corrupted binary data for RigCount"

504+

505+

493instance Binary ImplicitInfo where

506instance Binary ImplicitInfo where

494 put x

507 put x

495 = case x of

508 = case x of

@@ -504,10 +517,11 @@ instance (Binary b) => Binary (Binder b) where

504 = case x of

517 = case x of

505 Lam x1 -> do putWord8 0

518 Lam x1 -> do putWord8 0

506 put x1

519 put x1

507− Pi x1 x2 x3 -> do putWord8 1

520+ Pi x1 x2 x3 x4 -> do putWord8 1

508− put x1

521+ put x1

509− put x2

522+ put x2

510− put x3

523+ put x3

524+ put x4

511 Let x1 x2 -> do putWord8 2

525 Let x1 x2 -> do putWord8 2

512 put x1

526 put x1

513 put x2

527 put x2

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

523 Guess x1 x2 -> do putWord8 6

537 Guess x1 x2 -> do putWord8 6

524 put x1

538 put x1

525 put x2

539 put x2

526− PVar x1 -> do putWord8 7

540+ PVar x1 x2 -> do putWord8 7

527− put x1

541+ put x1

542+ put x2

528 PVTy x1 -> do putWord8 8

543 PVTy x1 -> do putWord8 8

529 put x1

544 put x1

530 get

545 get

@@ -535,7 +550,8 @@ instance (Binary b) => Binary (Binder b) where

535 1 -> do x1 <- get

550 1 -> do x1 <- get

536 x2 <- get

551 x2 <- get

537 x3 <- get

552 x3 <- get

553+ x4 <- get

538− return (Pi x1 x2 x3)

554+ return (Pi x1 x2 x3 x4)

539 2 -> do x1 <- get

555 2 -> do x1 <- get

540 x2 <- get

556 x2 <- get

541 return (Let x1 x2)

557 return (Let x1 x2)

@@ -552,7 +568,8 @@ instance (Binary b) => Binary (Binder b) where

552 x2 <- get

568 x2 <- get

553 return (Guess x1 x2)

569 return (Guess x1 x2)

554 7 -> do x1 <- get

570 7 -> do x1 <- get

571+ x2 <- get

555− return (PVar x1)

572+ return (PVar x1 x2)

556 8 -> do x1 <- get

573 8 -> do x1 <- get

557 return (PVTy x1)

574 return (PVTy x1)

558 _ -> error "Corrupted binary data for Binder"

575 _ -> error "Corrupted binary data for Binder"

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

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

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

393 | otherwise = PConst x

394

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

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

396 | reflect && noOccurrence n sc

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

398

src/Idris/Core/DeepSeq.hs+1

@@ -40,6 +40,7 @@ instance NFData ConstraintFC

40instance NFData Err

41instance NFData ErrorReportPart

42instance NFData ImplicitInfo

43+instance NFData RigCount

43instance (NFData b) => NFData (Binder b)

44instance (NFData b) => NFData (Binder b)

44instance NFData UExp

45instance NFData UExp

45instance NFData NameType

46instance NFData NameType

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

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

327 isInj ctxt (App _ f a) = isInj ctxt f

328 isInj ctxt (Constant _) = True

329 isInj ctxt (TType _) = True

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

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

331 isInj ctxt _ = False

332

333-- | get implementation argument names

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

589 return $! claims

590 where

591 argsOK :: Type -> [a] -> Bool

592− argsOK (Bind n (Pi _ _ _) sc) (i : is) = argsOK sc is

592+ argsOK (Bind n (Pi _ _ _ _) sc) (i : is) = argsOK sc is

593 argsOK _ (i : is) = False

594 argsOK _ [] = True

595

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

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

599 -> [Name] -- ^ Hypotheses

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

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

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

602 do let t = rebind hs t_in

603 n <- getNameFrom (mkMN n')

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

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

712 priOrder _ Nothing = GT

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

714

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

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

716 do n <- unique_hole (mkMN n')

717 when (null claims) (start_unify n)

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

@@ -749,13 +749,13 @@ checkPiGoal n

749 ctxt <- get_context

750 env <- get_env

751 case (whnf ctxt env g) of

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

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

753 _ -> do a <- getNameFrom (sMN 0 "__pargTy")

754 b <- getNameFrom (sMN 0 "__pretTy")

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

756 claim a RType

757 claim b RType

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

758+ claim f (RBind n (Pi RigW Nothing (Var a) RType) (Var b))

759 movelast a

760 movelast b

761 fill (Var f)

@@ -775,7 +775,7 @@ infer_app infer fun arg str =

775 s <- getNameFrom (sMN 0 "is")

776 claim a RType

777 claim b RType

778− claim f (RBind (sMN 0 "_aX") (Pi Nothing (Var a) RType) (Var b))

778+ claim f (RBind (sMN 0 "_aX") (Pi RigW Nothing (Var a) RType) (Var b))

779 tm <- get_term

780 start_unify s

781 -- if 'infer' is set, we're assuming it's a simply typed application

@@ -826,7 +826,7 @@ dep_app fun arg str =

826 case whnf ctxt env fty of

827 -- if f gives a function type, unify our argument type with

828 -- f's expected argument type

829− Bind _ (Pi _ argty _) _ -> unifyGoal (forget argty)

829+ Bind _ (Pi _ _ argty _) _ -> unifyGoal (forget argty)

830 -- Can't infer a type for 'f', so fail here (and drop back to

831 -- simply typed application where we infer the type for f)

832 _ -> fail "Can't make type"

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

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

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

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

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

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

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

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

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

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

@@ -645,8 +645,8 @@ convEq ctxt holes topx topy = ceq [] topx topy where

645 ceq ps (Bind n (Lam t) (App _ x (P Bound n' _))) y

646 | n == n' = ceq ps x y

647

648− ceq ps (Bind n (PVar t) sc) y = ceq ps sc y

648+ ceq ps (Bind n (PVar _ t) sc) y = ceq ps sc y

649− ceq ps x (Bind n (PVar t) sc) = ceq ps x sc

649+ ceq ps x (Bind n (PVar _ t) sc) = ceq ps x sc

650 ceq ps (Bind n (PVTy t) sc) y = ceq ps sc y

651 ceq ps x (Bind n (PVTy t) sc) = ceq ps x sc

652

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

662 where

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

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

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

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

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

667 -- Special case for 'case' blocks - size of scope causes complications,

668 -- we only want to check the blocks themselves are valid and identical

@@ -999,7 +999,7 @@ simplifyCasedef n ei uctxt

999 _ -> return ctxt

1000 return uctxt { definitions = ctxt' }

1001 where

1002− depat acc (Bind n (PVar t) sc)

1002+ depat acc (Bind n (PVar _ t) sc)

1003 = depat (n : acc) (instantiate (P Bound n t) sc)

1004 depat acc x = (acc, x)

1005 debind (Right (x, y)) = let (vs, x') = depat [] x

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

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

92 b' <- fixBinder b

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

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

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

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

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

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

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

99 fixBinder (GHole i ns t) = GHole i ns <$> toTT t

100 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

101− fixBinder (PVar t) = PVar <$> toTT t

101+ fixBinder (PVar rig t) = PVar rig <$> toTT t

102 fixBinder (PVTy t) = PVTy <$> toTT t

103 newN n = do (ExecState hs ns) <- lift get

104 let n' = uniqueName n ns

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

@@ -392,7 +392,7 @@ claimFn n bn argty ctxt env t@(Bind x (Hole retty) sc) =

392 lift $ isType ctxt env tyt

393 action (\ps -> let (g:gs) = holes ps in

394 ps { holes = g : n : gs } )

395− return $ Bind n (Hole (Bind bn (Pi Nothing tyv tyt) retty)) t

395+ return $ Bind n (Hole (Bind bn (Pi RigW Nothing tyv tyt) retty)) t

396claimFn _ _ _ ctxt env _ = fail "Can't make function type here"

397

398reorder_claims :: RunTactic

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

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

473 where

474 mkTy [] t = t

475− mkTy ((n,rig,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar [] 0))) (mkTy bs t)

475+ mkTy ((n,rig,b) : bs) t = Bind n (Pi RigW Nothing (binderTy b) (TType (UVar [] 0))) (mkTy bs t)

476

477 getP (n, rig, b) = P Bound n (binderTy b)

478defer dropped n ctxt env _ = fail "Can't defer a non-hole focus."

@@ -541,7 +541,7 @@ fill guess ctxt env (Bind x (Hole ty) sc) =

541 -- some expected types show up commonly in errors and indicate a

542 -- specific problem.

543 -- argTy -> retTy suggests a function applied to too many arguments

544− chkPurpose val (Bind _ (Pi _ (P _ (MN _ _) _) _) (P _ (MN _ _) _))

544+ chkPurpose val (Bind _ (Pi _ _ (P _ (MN _ _) _) _) (P _ (MN _ _) _))

545 = TooManyArgs val

546 chkPurpose _ _ = ExpectedType

547fill _ _ _ _ = fail "Can't fill here."

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

652 Just name -> name

653 Nothing -> x

654 let t' = case t of

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

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

656 _ -> normalise ctxt env t

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

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

659 case t' of

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

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

661 do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)

662 ps <- get

663 let (uh, uns) = unified ps

@@ -669,10 +669,10 @@ introTy ty n ctxt env _ = fail "Can't introduce here."

669intro :: Maybe Name -> RunTactic

670intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

671 do let t' = case t of

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

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

673 _ -> normalise ctxt env t

674 case t' of

675− Bind y (Pi _ s _) t ->

675+ Bind y (Pi _ _ s _) t ->

676 let n = case mn of

677 Just name -> name

678 Nothing -> y

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

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

690 unify' ctxt env (tyt, Nothing) (TType (UVar [] 0), Nothing)

691 unify' ctxt env (t, Nothing) (TType (UVar [] 0), Nothing)

692− return $ Bind n (Pi impl tyv (TType (UVar [] 0))) (Bind x (Hole t) (P Bound x t))

692+ return $ Bind n (Pi RigW impl tyv (TType (UVar [] 0))) (Bind x (Hole t) (P Bound x t))

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

694

695patvar :: Name -> RunTactic

@@ -702,7 +702,7 @@ patvar n ctxt env (Bind x (Hole t) sc) =

702 (notunified ps),

703 injective = addInj n x (injective ps)

704 })

705− return $ Bind n (PVar t) (updsubst x (P Bound n t) sc)

705+ return $ Bind n (PVar RigW t) (updsubst x (P Bound n t) sc)

706 where addInj n x ps | x `elem` ps = n : ps

707 | otherwise = ps

708patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm

@@ -830,7 +830,7 @@ patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

830 _ -> normalise ctxt env t

831 case t' of

832 Bind y (PVTy s) t -> let t' = updsubst y (P Bound n s) t in

833− return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))

833+ return $ Bind n (PVar RigW s) (Bind x (Hole t') (P Bound x t'))

834 _ -> fail "Nothing to pattern bind"

835patbind n ctxt env _ = fail "Can't pattern bind here"

836

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

@@ -854,7 +854,8 @@ deriving instance Binary ImplicitInfo

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

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

856 -- ^ A function binding

857+ | Pi { binderCount :: RigCount,

857− | Pi { binderImpl :: Maybe ImplicitInfo,

858+ binderImpl :: Maybe ImplicitInfo,

858 binderTy :: !b,

859 binderTy :: !b,

859 binderKind :: !b }

860 binderKind :: !b }

860 -- ^ A binding that occurs in a function type

861 -- ^ A binding that occurs in a function type

@@ -886,7 +887,8 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}

886 -- substituted - the guess is to keep it

887 -- substituted - the guess is to keep it

887 -- computationally inert while working on other things

888 -- computationally inert while working on other things

888 -- if necessary.

889 -- if necessary.

890+ | PVar { binderCount :: RigCount,

889− | PVar { binderTy :: !b }

891+ binderTy :: !b }

890 -- ^ A pattern variable (these are bound around terms

892 -- ^ A pattern variable (these are bound around terms

891 -- that make up pattern-match clauses)

893 -- that make up pattern-match clauses)

892 | PVTy { binderTy :: !b }

894 | PVTy { binderTy :: !b }

@@ -898,13 +900,13 @@ deriving instance Binary Binder

898

900

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

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

900 size (Lam ty) = 1 + size ty

902 size (Lam ty) = 1 + size ty

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

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

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

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

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

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

904 size (Hole ty) = 1 + size ty

906 size (Hole ty) = 1 + size ty

905 size (GHole _ _ ty) = 1 + size ty

907 size (GHole _ _ ty) = 1 + size ty

906 size (Guess ty val) = 1 + size ty + size val

908 size (Guess ty val) = 1 + size ty + size val

907− size (PVar ty) = 1 + size ty

909+ size (PVar _ ty) = 1 + size ty

908 size (PVTy ty) = 1 + size ty

910 size (PVTy ty) = 1 + size ty

909

911

910fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)

912fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)

@@ -912,10 +914,10 @@ fmapMB f (Let t v) = liftM2 Let (f t) (f v)

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

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

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

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

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

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

915−fmapMB f (Pi i t k) = liftM2 (Pi i) (f t) (f k)

917+fmapMB f (Pi c i t k) = liftM2 (Pi c i) (f t) (f k)

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

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

917fmapMB f (GHole i ns t) = liftM (GHole i ns) (f t)

919fmapMB f (GHole i ns t) = liftM (GHole i ns) (f t)

918−fmapMB f (PVar t) = liftM PVar (f t)

920+fmapMB f (PVar c t) = liftM (PVar c) (f t)

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

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

920

922

921raw_apply :: Raw -> [Raw] -> Raw

923raw_apply :: Raw -> [Raw] -> Raw

@@ -1127,7 +1129,7 @@ isInjective (P (DCon _ _ _) _ _) = True

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

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

1128isInjective (Constant _) = True

1130isInjective (Constant _) = True

1129isInjective (TType x) = True

1131isInjective (TType x) = True

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

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

1131isInjective (App _ f a) = isInjective f

1133isInjective (App _ f a) = isInjective f

1132isInjective _ = False

1134isInjective _ = False

1133

1135

@@ -1361,7 +1363,7 @@ freeNames t = nub $ freeNames' t

1361

1363

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

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

1363arity :: TT n -> Int

1365arity :: TT n -> Int

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

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

1365arity _ = 0

1367arity _ = 0

1366

1368

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

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

@@ -1457,22 +1459,22 @@ bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)

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

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

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

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

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

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

1460−getArgTys (Bind n (PVar _) sc) = getArgTys sc

1462+getArgTys (Bind n (PVar _ _) sc) = getArgTys sc

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

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

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

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

1463getArgTys _ = []

1465getArgTys _ = []

1464

1466

1465getRetTy :: TT n -> TT n

1467getRetTy :: TT n -> TT n

1466−getRetTy (Bind n (PVar _) sc) = getRetTy sc

1468+getRetTy (Bind n (PVar _ _) sc) = getRetTy sc

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

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

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

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

1469getRetTy sc = sc

1471getRetTy sc = sc

1470

1472

1471-- | As getRetTy but substitutes names for de Bruijn indices

1473-- | As getRetTy but substitutes names for de Bruijn indices

1472substRetTy :: TT n -> TT n

1474substRetTy :: TT n -> TT n

1473−substRetTy (Bind n (PVar ty) sc) = substRetTy (substV (P Ref n ty) sc)

1475+substRetTy (Bind n (PVar _ ty) sc) = substRetTy (substV (P Ref n ty) sc)

1474substRetTy (Bind n (PVTy ty) sc) = substRetTy (substV (P Ref n ty) sc)

1476substRetTy (Bind n (PVTy ty) sc) = substRetTy (substV (P Ref n ty) sc)

1475−substRetTy (Bind n (Pi _ ty _) sc) = substRetTy (substV (P Ref n ty) sc)

1477+substRetTy (Bind n (Pi _ _ ty _) sc) = substRetTy (substV (P Ref n ty) sc)

1476substRetTy sc = sc

1478substRetTy sc = sc

1477

1479

1478

1480

@@ -1589,7 +1591,7 @@ prettyEnv env t = prettyEnv' env t False

1589 else

1591 else

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

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

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

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

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

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

1593 | noOccurrence n sc && not debug =

1595 | noOccurrence n sc && not debug =

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

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

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

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

@@ -1609,8 +1611,11 @@ prettyEnv env t = prettyEnv' env t False

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

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

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

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

1611 prettySb env n (GHole _ _ t) = prettyB env "?gdefer" "." n t

1613 prettySb env n (GHole _ _ t) = prettyB env "?gdefer" "." n t

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

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

1615+ prettySb env n (Pi Rig1 _ t _) = prettyB env "(" ") -o" n t

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

1617+ prettySb env n (PVar Rig1 t) = prettyB env "pat 1 " "." n t

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

1618+ prettySb env n (PVar _ t) = prettyB env "pat" "." n t

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

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

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

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

1616 prettySb env n (NLet t v) = prettyBv env "nlet" "in" n t v

1621 prettySb env n (NLet t v) = prettyBv env "nlet" "in" n t v

@@ -1636,12 +1641,13 @@ showEnv' env t dbg = se 10 env t where

1636 = (show $ fstEnv $ env!!i) ++

1641 = (show $ fstEnv $ env!!i) ++

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

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

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

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

1639− se p env (Bind n b@(Pi (Just _) t k) sc)

1644+ se p env (Bind n b@(Pi rig (Just _) t k) sc)

1640− = bracket p 2 $ sb env n b ++ se 10 ((n,Rig0,b):env) sc

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

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

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

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

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

1643− where arrow (TType _) = " -> "

1648+ where arrow Rig0 = " -> "

1644− arrow u = " [" ++ show u ++ "] -> "

1649+ arrow Rig1 = " -o "

1650+ arrow RigW = " -> "

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

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

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

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

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

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

@@ -1655,9 +1661,12 @@ showEnv' env t dbg = se 10 env t where

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

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

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

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

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

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

1658− sb env n (Pi (Just _) t _) = showb env "{" "} -> " n t

1664+ sb env n (Pi Rig1 (Just _) t _) = showb env "{" "} -o " n t

1665+ sb env n (Pi _ (Just _) t _) = showb env "{" "} -> " n t

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

1666+ sb env n (Pi Rig1 _ t _) = showb env "(" ") -0 " n t

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

1668+ sb env n (PVar Rig1 t) = showb env "pat 1 " ". " n t

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

1669+ sb env n (PVar _ t) = showb env "pat " ". " n t

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

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

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

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

1663 sb env n (NLet t v) = showbv env "nlet " " in " n t v

1672 sb env n (NLet t v) = showbv env "nlet " " in " n t v

@@ -1765,13 +1774,13 @@ pprintTT bound tm = pp startPrec bound tm

1765 ppb p bound n (Lam ty) sc =

1774 ppb p bound n (Lam ty) sc =

1766 bracket p startPrec . group . align . hang 2 $

1775 bracket p startPrec . group . align . hang 2 $

1767 text "λ" <+> bindingOf n False <+> text "." <> line <> sc

1776 text "λ" <+> bindingOf n False <+> text "." <> line <> sc

1768− ppb p bound n (Pi _ ty k) sc =

1777+ ppb p bound n (Pi rig _ ty k) sc =

1769 bracket p startPrec . group . align $

1778 bracket p startPrec . group . align $

1770 lparen <> (bindingOf n False) <+> colon <+>

1779 lparen <> (bindingOf n False) <+> colon <+>

1771 (group . align) (pp startPrec bound ty) <>

1780 (group . align) (pp startPrec bound ty) <>

1772− rparen <+> mkArrow k <> line <> sc

1781+ rparen <+> mkArrow rig <> line <> sc

1773− where mkArrow (UType UniqueType) = text "⇴"

1782+ where mkArrow Rig1 = text "⇴"

1774− mkArrow (UType NullType) = text "⥛"

1783+ mkArrow Rig0 = text "⥛"

1775 mkArrow _ = text "→"

1784 mkArrow _ = text "→"

1776 ppb p bound n (Let ty val) sc =

1785 ppb p bound n (Let ty val) sc =

1777 bracket p startPrec . group . align $

1786 bracket p startPrec . group . align $

@@ -1800,7 +1809,7 @@ pprintTT bound tm = pp startPrec bound tm

1800 text "?" <> bindingOf n False <+>

1809 text "?" <> bindingOf n False <+>

1801 text "≈" <+> pp startPrec bound val <+>

1810 text "≈" <+> pp startPrec bound val <+>

1802 text "." <> line <> sc

1811 text "." <> line <> sc

1803− ppb p bound n (PVar ty) sc =

1812+ ppb p bound n (PVar _ ty) sc =

1804 bracket p startPrec . group . align . hang 2 $

1813 bracket p startPrec . group . align . hang 2 $

1805 annotate AnnKeyword (text "pat") <+>

1814 annotate AnnKeyword (text "pat") <+>

1806 bindingOf n False <+> colon <+> pp startPrec bound ty <+>

1815 bindingOf n False <+> colon <+> pp startPrec bound ty <+>

@@ -1853,8 +1862,8 @@ pprintRaw bound (RBind n b body) =

1853 where

1862 where

1854 ppb (Lam ty) = enclose lparen rparen . group . align . hang 2 $

1863 ppb (Lam ty) = enclose lparen rparen . group . align . hang 2 $

1855 text "Lam" <$> pprintRaw bound ty

1864 text "Lam" <$> pprintRaw bound ty

1856− ppb (Pi _ ty k) = enclose lparen rparen . group . align . hang 2 $

1865+ ppb (Pi _ _ ty k) = enclose lparen rparen . group . align . hang 2 $

1857− vsep [text "Pi", pprintRaw bound ty, pprintRaw bound k]

1866+ vsep [text "Pi", pprintRaw bound ty, pprintRaw bound k]

1858 ppb (Let ty v) = enclose lparen rparen . group . align . hang 2 $

1867 ppb (Let ty v) = enclose lparen rparen . group . align . hang 2 $

1859 vsep [text "Let", pprintRaw bound ty, pprintRaw bound v]

1868 vsep [text "Let", pprintRaw bound ty, pprintRaw bound v]

1860 ppb (NLet ty v) = enclose lparen rparen . group . align . hang 2 $

1869 ppb (NLet ty v) = enclose lparen rparen . group . align . hang 2 $

@@ -1865,8 +1874,8 @@ pprintRaw bound (RBind n b body) =

1865 text "GHole" <$> pprintRaw bound ty

1874 text "GHole" <$> pprintRaw bound ty

1866 ppb (Guess ty v) = enclose lparen rparen . group . align . hang 2 $

1875 ppb (Guess ty v) = enclose lparen rparen . group . align . hang 2 $

1867 vsep [text "Guess", pprintRaw bound ty, pprintRaw bound v]

1876 vsep [text "Guess", pprintRaw bound ty, pprintRaw bound v]

1868− ppb (PVar ty) = enclose lparen rparen . group . align . hang 2 $

1877+ ppb (PVar _ ty) = enclose lparen rparen . group . align . hang 2 $

1869− text "PVar" <$> pprintRaw bound ty

1878+ text "PVar" <$> pprintRaw bound ty

1870 ppb (PVTy ty) = enclose lparen rparen . group . align . hang 2 $

1879 ppb (PVTy ty) = enclose lparen rparen . group . align . hang 2 $

1871 text "PVTy" <$> pprintRaw bound ty

1880 text "PVTy" <$> pprintRaw bound ty

1872pprintRaw bound (RApp f x) =

1881pprintRaw bound (RApp f x) =

src/Idris/Core/Typecheck.hs+27−25

@@ -114,19 +114,19 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

114 -- special case to reduce constraintss

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

116 let fty' = case uniqueBinders (map fstEnv env) (finalise fty) of

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

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

118 _ -> uniqueBinders (map fstEnv env)

119 $ case normalise ctxt env fty of

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

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

121 _ -> normalise ctxt env fty

122 case fty' of

123− Bind x (Pi i (TType v') k) t ->

123+ Bind x (Pi rig i (TType v') k) t ->

124 do (v, cs) <- get

125 put (v+1, ULT (UVar tcns v) v' : cs)

126 let apty = simplify initContext env

127 (Bind x (Let (TType v') (TType (UVar tcns v))) t)

128 return (App Complete fv (TType (UVar tcns v)), apty)

129− Bind x (Pi i s k) t ->

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

130 do (av, aty) <- chk u Nothing env RType

131 convertsC ctxt env aty s

132 let apty = simplify initContext env

@@ -136,14 +136,14 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

136 chk u lvl env ap@(RApp f a)

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

138 let fty' = case uniqueBinders (map fstEnv env) (finalise fty) of

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

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

140 _ -> uniqueBinders (map fstEnv env)

141 $ case normalise ctxt env fty of

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

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

143 _ -> normalise ctxt env fty

144 (av, aty) <- chk u Nothing env a

145 case fty' of

146− Bind x (Pi i s k) t ->

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

147 do convertsC ctxt env aty s

148 let apty = simplify initContext env

149 (Bind x (Let aty av) t)

@@ -178,7 +178,7 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

178 constType TheWorld = Constant WorldType

179 constType Forgot = Erased

180 constType _ = TType (UVal 0)

181− chk u lvl env (RBind n (Pi i s k) t)

181+ chk u lvl env (RBind n (Pi rig i s k) t)

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

183 (v, cs) <- get

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

@@ -186,8 +186,7 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

186 let maxu = case lvl of

187 Nothing -> UVar tcns v

188 Just v' -> v'

189− -- TODO: Get RigCount from Pi

190− (tv, tt) <- chk st (Just maxu) ((n, Rig0, Pi i sv kv) : env) t

189+ (tv, tt) <- chk st (Just maxu) ((n, rig, Pi rig i sv kv) : env) t

191

190

192-- convertsC ctxt env st (TType maxu)

191-- convertsC ctxt env st (TType maxu)

193-- convertsC ctxt env tt (TType maxu)

192-- convertsC ctxt env tt (TType maxu)

@@ -201,16 +200,16 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

201 put (v, ULE su maxu :

200 put (v, ULE su maxu :

202 ULE tu maxu : cs)

201 ULE tu maxu : cs)

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

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

204− return (Bind n (Pi i (uniqueBinders (map fstEnv env) sv) k')

203+ return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')

205 (pToV n tv), k')

204 (pToV n tv), k')

206 (un, un') ->

205 (un, un') ->

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

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

208− return (Bind n (Pi i (uniqueBinders (map fstEnv env) sv) k')

207+ return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')

209 (pToV n tv), k')

208 (pToV n tv), k')

210

209

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

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

212 = let k' = smaller kv k in

211 = let k' = smaller kv k in

213− Bind n (Pi i s k') (mkUniquePi k' sc)

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

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

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

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

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

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

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

@@ -220,15 +219,18 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

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

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

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

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

222 mostUnique [] k = k

221 mostUnique [] k = k

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

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

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

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

225

224

226 chk u lvl env (RBind n b sc)

225 chk u lvl env (RBind n b sc)

227 = do (b', bt') <- checkBinder b

226 = do (b', bt') <- checkBinder b

228− -- TODO: Get RigCount from binder (Pi or Pattern?)

229− (scv, sct) <- chk (smaller bt' u) Nothing ((n, Rig0, b'):env) sc

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

230 discharge n b' bt' (pToV n scv) (pToV n sct)

228 discharge n b' bt' (pToV n scv) (pToV n sct)

229+ where getCount (Pi rig _ _ _) = rig

230+ getCount (PVar rig _) = rig

231+ getCount _ = Rig0

232+

231− where checkBinder (Lam t)

233+ checkBinder (Lam t)

232 = do (tv, tt) <- chk u Nothing env t

234 = do (tv, tt) <- chk u Nothing env t

233 let tv' = normalise ctxt env tv

235 let tv' = normalise ctxt env tv

234 convType tcns ctxt env tt

236 convType tcns ctxt env tt

@@ -268,13 +270,13 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

268 convertsC ctxt env vt tv

270 convertsC ctxt env vt tv

269 convType tcns ctxt env tt

271 convType tcns ctxt env tt

270 return (Guess tv vv, tt)

272 return (Guess tv vv, tt)

271− checkBinder (PVar t)

273+ checkBinder (PVar rig t)

272 = do (tv, tt) <- chk u Nothing env t

274 = do (tv, tt) <- chk u Nothing env t

273 let tv' = normalise ctxt env tv

275 let tv' = normalise ctxt env tv

274 convType tcns ctxt env tt

276 convType tcns ctxt env tt

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

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

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

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

277− return (PVar tv, tt)

279+ return (PVar rig tv, tt)

278 checkBinder (PVTy t)

280 checkBinder (PVTy t)

279 = do (tv, tt) <- chk u Nothing env t

281 = do (tv, tt) <- chk u Nothing env t

280 let tv' = normalise ctxt env tv

282 let tv' = normalise ctxt env tv

@@ -282,9 +284,9 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

282 return (PVTy tv, tt)

284 return (PVTy tv, tt)

283

285

284 discharge n (Lam t) bt scv sct

286 discharge n (Lam t) bt scv sct

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

287+ = return (Bind n (Lam t) scv, Bind n (Pi RigW Nothing t bt) sct)

286− discharge n (Pi i t k) bt scv sct

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

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

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

288 discharge n (Let t v) bt scv sct

290 discharge n (Let t v) bt scv sct

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

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

290 discharge n (NLet t v) bt scv sct

292 discharge n (NLet t v) bt scv sct

@@ -295,8 +297,8 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

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

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

296 discharge n (Guess t v) bt scv sct

298 discharge n (Guess t v) bt scv sct

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

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

298− discharge n (PVar t) bt scv sct

300+ discharge n (PVar r t) bt scv sct

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

301+ = return (Bind n (PVar r t) scv, Bind n (PVTy t) sct)

300 discharge n (PVTy t) bt scv sct

302 discharge n (PVTy t) bt scv sct

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

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

302

304

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

@@ -141,7 +141,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

141 h2 <- un bnames vx vy

142 combine bnames h1 h2

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

144− uB bnames (Pi i tx _) (Pi i' ty _) = un bnames tx ty

144+ uB bnames (Pi r i tx _) (Pi r' i' ty _) = un bnames tx ty

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

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

147 (normalise ctxt env (binderTy y))

@@ -491,18 +491,18 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

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

492 -- interface resolution for interfaces over functions.

493

494− un' env fn bnames (App _ f x) (Bind n (Pi i t k) y)

494+ un' env fn bnames (App _ f x) (Bind n (Pi r i t k) y)

495 | noOccurrence n y && injectiveApp f

496 = do ux <- un' env False bnames x y

497 uf <- un' env False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar [] 0)))

498− (Bind n (Pi i t k) (V 1)))

498+ (Bind n (Pi r i t k) (V 1)))

499 combine env bnames ux uf

500

501− un' env fn bnames (Bind n (Pi i t k) y) (App _ f x)

501+ un' env fn bnames (Bind n (Pi r i t k) y) (App _ f x)

502 | noOccurrence n y && injectiveApp f

503 = do ux <- un' env False bnames y x

504 uf <- un' env False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar [] 0)))

505− (Bind n (Pi i t k) (V 1))) f

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

506 combine env bnames ux uf

507

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

@@ -511,7 +511,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

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

512 combine env bnames h1 h2

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

514− sameBinder (Pi i _ _) (Pi i' _ _) = True

514+ sameBinder (Pi _ i _ _) (Pi _ i' _ _) = True

515 sameBinder _ _ = False -- never unify holes/guesses/etc

516 un' env fn bnames x y

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

@@ -643,9 +643,9 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

643 sc 1

644 combine env bnames h1 h2

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

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

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

647 uB env bnames (Hole tx) (Hole ty) = un' env False bnames tx ty

648− uB env bnames (PVar tx) (PVar ty) = un' env False bnames tx ty

648+ uB env bnames (PVar _ tx) (PVar _ ty) = un' env False bnames tx ty

649 uB env bnames x y

650 = do UI s f <- get

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

@@ -754,13 +754,13 @@ recoverable (App _ f a) (App _ f' a')

754 | f == f' = recoverable a a'

755recoverable (App _ f a) (App _ f' a')

756 = recoverable f f' -- && recoverable a a'

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

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

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

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

760 | (Constant _) <- f = False

761 | TType _ <- f = False

762 | UType _ <- f = False

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

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

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

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

766 | (Constant _) <- f = False

@@ -781,6 +781,6 @@ holeIn env n = case lookupBinder n env of

781

782patIn :: Env -> Name -> Bool

783patIn env n = case lookupBinder n env of

784− Just (PVar _) -> True

784+ Just (PVar _ _) -> True

785 Just (PVTy _) -> True

786 _ -> False

src/Idris/Core/WHNF.hs+2−3

@@ -72,9 +72,8 @@ whnfArgs' ctxt env tm

72 -- The assumption is that de Bruijn indices refer to local things

73 -- (so not in the external environment) so we need to instantiate

74 -- the name

75− Bind n b@(Pi _ ty _) sc ->

75+ Bind n b@(Pi rig _ ty _) sc ->

76− -- TODO: Get RigCount from Pi

77− Bind n b (whnfArgs' ctxt ((n,Rig0,b):env)

76+ Bind n b (whnfArgs' ctxt ((n, rig, b):env)

78 (subst n (P Bound n ty) sc))

77 (subst n (P Bound n ty) sc))

79 res -> tm

78 res -> tm

80

79

src/Idris/Delaborate.hs+9−9

@@ -137,26 +137,26 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

137 _ -> PRef un [] n

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

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

140− de env (_ : is) (Bind n (Pi (Just impl) ty _) sc)

140+ de env (_ : is) (Bind n (Pi rig (Just impl) ty _) sc)

141 | toplevel_imp impl -- information in 'imps' repeated

142 = PPi (Imp [] Dynamic False (Just impl) False) n NoFC (de env [] ty) (de ((n,n):env) is sc)

143− de env is (Bind n (Pi (Just impl) ty _) sc)

143+ de env is (Bind n (Pi rig (Just impl) ty _) sc)

144 | tcimplementation impl

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

146 | otherwise

147 = PPi (Imp [] Dynamic False (Just impl) False) n NoFC (de env [] ty) (de ((n,n):env) is sc)

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

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

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

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

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

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

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

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

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

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

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

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

156 n NoFC

157 (de env [] ty)

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

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

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

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

161

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

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

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

340 y)) <>

341 if (opt_errContext (idris_options i)) then line <> text "Conversion failure" <$> showSc i env else empty

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

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

343 = App Complete (P Ref (sUN (show u)) Erased)

344− (Bind n (Pi i (flagUnique t) k) (flagUnique sc))

344+ (Bind n (Pi rig i (flagUnique t) k) (flagUnique sc))

345 flagUnique (App s f a) = App s (flagUnique f) (flagUnique a)

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

347 flagUnique t = t

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

@@ -329,12 +329,12 @@ elabClauses info' fc opts n_in cs =

329 debind (Left x) = let (vs, x') = depat [] x in

330 (vs, x', Impossible)

331

332− depat acc (Bind n (PVar t) sc) = depat ((n, t) : acc) (instantiate (P Bound n t) sc)

332+ depat acc (Bind n (PVar rig t) sc) = depat ((n, t) : acc) (instantiate (P Bound n t) sc)

333 depat acc x = (acc, x)

334

335

336− getPVs (Bind x (PVar _) tm) = let (vs, tm') = getPVs tm

336+ getPVs (Bind x (PVar rig _) tm) = let (vs, tm') = getPVs tm

337− in (x:vs, tm')

337+ in (x:vs, tm')

338 getPVs tm = ([], tm)

339

340 isPatVar vs (P Bound n _) = n `elem` vs

@@ -529,7 +529,7 @@ elabPE info fc caller r =

529 _ -> True

530 concreteTm ist (Constant _) = True

531 concreteTm ist (Bind n (Lam _) sc) = True

532− concreteTm ist (Bind n (Pi _ _ _) sc) = True

532+ concreteTm ist (Bind n (Pi _ _ _ _) sc) = True

533 concreteTm ist (Bind n (Let _ _) sc) = concreteTm ist sc

534 concreteTm ist _ = False

535

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

1106 let wargname = sMN windex "warg"

1107

1108 logElab 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)

1109− let wtype = bindTyArgs (flip (Pi Nothing) (TType (UVar [] 0))) (bargs_pre ++

1109+ let wtype = bindTyArgs (flip (Pi RigW Nothing) (TType (UVar [] 0))) (bargs_pre ++

1110 (wargname, wargtype) :

1111 map (abstract wargname wargval wargtype) bargs_post ++

1112 case mpn of

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

1200 (crhs, crhsty) <- recheckC (constraintNS info) fc id [] rhs'

1201 return (Right (clhs, crhs), lhs)

1202 where

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

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

1204 getImps _ = []

1205

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

@@ -1299,13 +1299,13 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

1299 -- This is something of a hack, because matching on the top level

1300 -- application won't find this information for us

1301 addResolvesArgs :: FC -> Term -> [PArg] -> [PArg]

1302− addResolvesArgs fc (Bind n (Pi _ ty _) sc) (a : args)

1302+ addResolvesArgs fc (Bind n (Pi _ _ ty _) sc) (a : args)

1303 | (P _ cn _, _) <- unApply ty,

1304 getTm a == Placeholder

1305 = case lookupCtxtExact cn (idris_interfaces ist) of

1306 Just _ -> a { getTm = PResolveTC fc } : addResolvesArgs fc sc args

1307 Nothing -> a : addResolvesArgs fc sc args

1308− addResolvesArgs fc (Bind n (Pi _ ty _) sc) (a : args)

1308+ addResolvesArgs fc (Bind n (Pi _ _ ty _) sc) (a : args)

1309 = a : addResolvesArgs fc sc args

1310 addResolvesArgs fc _ args = args

1311

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

@@ -267,7 +267,7 @@ forceArgs ctxt ty = forceFrom 0 ty

267 -- then when we look at the return type, if we see MN pos name

268 -- constructor guarded, then 'pos' is a forceable position

269 forceFrom :: Int -> Type -> [Int]

270− forceFrom i (Bind n (Pi _ _ _) sc)

270+ forceFrom i (Bind n (Pi _ _ _ _) sc)

271 = forceFrom (i + 1) (substV (P Ref (sMN i "FF") Erased) sc)

272 forceFrom i sc

273 -- Go under the top level type application

@@ -310,7 +310,7 @@ addParamConstraints fc ps cty cons

310 where

311 getParamNames (n, ty) = (ty, getPs ty)

312

313− getPs (Bind n (Pi _ _ _) sc)

313+ getPs (Bind n (Pi _ _ _ _) sc)

314 = getPs (substV (P Ref n Erased) sc)

315 getPs t | (f, args) <- unApply t

316 = paramArgs 0 args

@@ -321,7 +321,7 @@ addParamConstraints fc ps cty cons

321

322 addConConstraint ps cvar (ty, pnames) = constraintTy ty

323 where

324− constraintTy (Bind n (Pi _ ty _) sc)

324+ constraintTy (Bind n (Pi _ _ ty _) sc)

325 = case getRetTy ty of

326 TType avar -> do tit <- typeInType

327 when (not tit) $ do

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

@@ -516,6 +516,6 @@ checkInjectiveArgs fc n ds (Just ty)

516 isInj i (Bind n b sc) = isInj i sc

517 isInj _ _ = True

518

519− instantiateRetTy (Bind n (Pi _ _ _) sc)

519+ instantiateRetTy (Bind n (Pi _ _ _ _) sc)

520 = substV (P Bound n Erased) (instantiateRetTy sc)

521 instantiateRetTy t = t

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

@@ -376,7 +376,7 @@ findDets n ns =

376 Just ty -> getDetPos 0 ns ty

377 Nothing -> []

378 where

379− getDetPos i ns (Bind n (Pi _ _ _) sc)

379+ getDetPos i ns (Bind n (Pi _ _ _ _) sc)

380 | n `elem` ns = i : getDetPos (i + 1) ns sc

381 | otherwise = getDetPos (i + 1) ns sc

382 getDetPos _ _ _ = []

src/Idris/Elab/Rewrite.hs+6−6

@@ -156,10 +156,10 @@ data ParamInfo = Index

156

157getParamInfo :: Type -> [PArg] -> Int -> [Int] -> [ParamInfo]

158-- Skip the top level implicits, we just need the explicit ones

159−getParamInfo (Bind n (Pi _ _ _) sc) (PExp{} : is) i ps

159+getParamInfo (Bind n (Pi _ _ _ _) sc) (PExp{} : is) i ps

160 | i `elem` ps = Param : getParamInfo sc is (i + 1) ps

161 | otherwise = Index : getParamInfo sc is (i + 1) ps

162−getParamInfo (Bind n (Pi _ _ _) sc) (_ : is) i ps

162+getParamInfo (Bind n (Pi _ _ _ _) sc) (_ : is) i ps

163 | i `elem` ps = ImplicitParam : getParamInfo sc is (i + 1) ps

164 | otherwise = ImplicitIndex : getParamInfo sc is (i + 1) ps

165getParamInfo _ _ _ _ = []

@@ -249,13 +249,13 @@ mkLemma info lemma tcon ps ty =

249 mkArgs _ _ _ = []

250

251 bindIdxs ist [] ty is tm = tm

252− bindIdxs ist (Param : pinfo) (Bind n (Pi _ ty _) sc) is tm

252+ bindIdxs ist (Param : pinfo) (Bind n (Pi _ _ ty _) sc) is tm

253 = bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm

254− bindIdxs ist (Index : pinfo) (Bind n (Pi _ ty _) sc) (i : is) tm

254+ bindIdxs ist (Index : pinfo) (Bind n (Pi _ _ ty _) sc) (i : is) tm

255 = PPi forall_imp i fc (delab ist ty)

256 (bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm)

257− bindIdxs ist (ImplicitParam : pinfo) (Bind n (Pi _ ty _) sc) is tm

257+ bindIdxs ist (ImplicitParam : pinfo) (Bind n (Pi _ _ ty _) sc) is tm

258 = bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm

259− bindIdxs ist (ImplicitIndex : pinfo) (Bind n (Pi _ ty _) sc) (i : is) tm

259+ bindIdxs ist (ImplicitIndex : pinfo) (Bind n (Pi _ _ ty _) sc) (i : is) tm

260 = bindIdxs ist pinfo (instantiate (P Bound n ty) sc) is tm

261 bindIdxs _ _ _ _ tm = tm

src/Idris/Elab/Term.hs+12−12

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

201 Nothing -> []

202 Just ty -> checkArgs [] [] ty

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

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

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

205 = let env' = case t of

206 TType _ -> n : env

207 _ -> env in

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

810 ans <- claimArgTys env xs

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

812 fnTy [] ret = forget ret

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

813+ fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi RigW Nothing xt RType) (fnTy xs ret)

814

815 localVar env (PRef _ _ x)

816 = case lookupBinder x env of

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

957 = lift $ tfail $ UnknownImplicit (pname imp) f

958 checkKnownImplicit _ = return ()

959

960− getReqImps (Bind x (Pi (Just i) ty _) sc)

960+ getReqImps (Bind x (Pi _ (Just i) ty _) sc)

961 = i : getReqImps sc

962 getReqImps _ = []

963

@@ -1484,12 +1484,12 @@ elab ist info emode opts fn tm

1484 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

1485 fullApp x = x

1486

1487− insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs

1487+ insertScopedImps fc (Bind n (Pi _ im@(Just i) _ _) sc) xs

1488 | tcimplementation i && not (toplevel_imp i)

1489 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs

1490 | not (toplevel_imp i)

1491 = pimp n Placeholder True : insertScopedImps fc sc xs

1492− insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)

1492+ insertScopedImps fc (Bind n (Pi _ _ _ _) sc) (x : xs)

1493 = x : insertScopedImps fc sc xs

1494 insertScopedImps _ _ xs = xs

1495

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

1500 addLam ty' t

1501 where

1502 -- just one level at a time

1503− addLam (Bind n (Pi (Just _) _ _) sc) t =

1503+ addLam (Bind n (Pi _ (Just _) _ _) sc) t =

1504 do impn <- unique_hole n -- (sMN 0 "scoped_imp")

1505 if e_isfn ina -- apply to an implicit immediately

1506 then return (PApp emptyFC

@@ -1782,7 +1782,7 @@ isPlausible ist var env n ty

1782 where

1783 collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->

1784 (Maybe Name, [(Term, [Name])])

1785− collectConstraints env tcs (Bind n (Pi _ ty _) sc)

1785+ collectConstraints env tcs (Bind n (Pi _ _ ty _) sc)

1786 = let tcs' = case unApply ty of

1787 (P _ c _, _) ->

1788 case lookupCtxtExact c (idris_interfaces ist) of

@@ -1916,7 +1916,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm

1916 returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)

1917

1918 patvars :: [(Name, Term)] -> Term -> ([(Name, Term)], Term)

1919− patvars ns (Bind n (PVar t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc)

1919+ patvars ns (Bind n (PVar _ t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc)

1920 patvars ns tm = (ns, tm)

1921

1922 pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term)

@@ -1985,7 +1985,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm

1985

1986 -- | Add another argument to a Pi

1987 mkPi :: RFunArg -> Raw -> Raw

1988− mkPi arg rTy = RBind (argName arg) (Pi Nothing (argTy arg) (RUType AllTypes)) rTy

1988+ mkPi arg rTy = RBind (argName arg) (Pi RigW Nothing (argTy arg) (RUType AllTypes)) rTy

1989

1990 mustBeType ctxt tm ty =

1991 case normaliseAll ctxt [] (finalise ty) of

@@ -2042,7 +2042,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm

2042 _ -> n

2043

2044 getRetTy :: Type -> Type

2045− getRetTy (Bind _ (Pi _ _ _) sc) = getRetTy sc

2045+ getRetTy (Bind _ (Pi _ _ _ _) sc) = getRetTy sc

2046 getRetTy ty = ty

2047

2048 elabScriptStuck :: Term -> ElabD a

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

2617 where tacticTy = Var (reflm "Tactic")

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

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

2620− (Pi Nothing (RApp listTy envTupleType) RType)

2620+ (Pi RigW Nothing (RApp listTy envTupleType) RType)

2621 (RBind (sMN 1 "__pi_arg")

2622− (Pi Nothing (Var $ reflm "TT") RType) tacticTy))

2622+ (Pi RigW Nothing (Var $ reflm "TT") RType) tacticTy))

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

2624 -- goal, then apply the resulting reflected Tactic

2625 = do tgoal <- goal

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

@@ -114,11 +114,11 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

114 return (clhs_tm, crhs_tm)

115

116 where

117− depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)

117+ depat (Bind n (PVar _ t) sc) = depat (instantiate (P Bound n t) sc)

118 depat x = x

119

120− renamepats (n' : ns) (Bind n (PVar t) sc)

120+ renamepats (n' : ns) (Bind n (PVar rig t) sc)

121− = Bind n' (PVar t) (renamepats ns sc) -- all Vs

121+ = Bind n' (PVar rig t) (renamepats ns sc) -- all Vs

122 renamepats _ sc = sc

123

124 -- names for transformation variables. Need to ensure these don't clash

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

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

135

136 return (cty, ckind, ty, inacc)

137 where

138− patToImp (Bind n (PVar t) sc) = Bind n (Pi Nothing t (TType (UVar [] 0))) (patToImp sc)

138+ patToImp (Bind n (PVar rig t) sc) = Bind n (Pi rig Nothing t (TType (UVar [] 0))) (patToImp sc)

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

140 patToImp t = t

141

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

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

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

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

145 param_pos i ns t = []

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

260 lst = txt "List"

261 errrep = txt "ErrorReportPart"

262

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

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

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

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

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

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

@@ -103,7 +103,7 @@ checkAddDef add toplvl info fc mkerr definable ((n, (i, top, t, psns)) : ns)

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

104-- type

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

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

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

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

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

109inaccessibleImps _ _ _ = []

@@ -184,7 +184,7 @@ decorateid decorate (PClauses f o n cs)

184

185-- if 't' is an interface application, assume its arguments are injective

186pbinds :: IState -> Term -> ElabD ()

187−pbinds i (Bind n (PVar t) sc)

187+pbinds i (Bind n (PVar _ t) sc)

188 = do attack; patbind n

189 env <- get_env

190 case unApply (normalise (tt_ctxt i) env t) of

@@ -198,26 +198,26 @@ pbinds i (Bind n (PVar t) sc)

198 setinjArg _ = return ()

199pbinds i tm = return ()

200

201−pbty (Bind n (PVar t) sc) tm = Bind n (PVTy t) (pbty sc tm)

201+pbty (Bind n (PVar _ t) sc) tm = Bind n (PVTy t) (pbty sc tm)

202pbty _ tm = tm

203

204−getPBtys (Bind n (PVar t) sc) = (n, t) : getPBtys sc

204+getPBtys (Bind n (PVar _ t) sc) = (n, t) : getPBtys sc

205getPBtys (Bind n (PVTy t) sc) = (n, t) : getPBtys sc

206getPBtys _ = []

207

208−psolve (Bind n (PVar t) sc) = do solve; psolve sc

208+psolve (Bind n (PVar _ t) sc) = do solve; psolve sc

209psolve tm = return ()

210

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

211+pvars ist (Bind n (PVar _ t) sc) = (n, delab ist t) : pvars ist sc

212pvars ist _ = []

213

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

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

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

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

217 ++ case unApply t of

218 (P _ n _, _) -> if n `elem` env then [n] else []

219 _ -> []

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

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

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

222getFixedInType i env is tm@(App _ f a)

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

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

231 getFixedInType i env is a

232getFixedInType i _ _ _ = []

233

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

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

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

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

237

@@ -260,7 +260,7 @@ getParamsInType i env ps t = let fix = getFixedInType i env ps t

260 flex = getFlexInType i env fix t in

261 [x | x <- fix, not (x `elem` flex)]

262

263−getTCinj i (Bind n (Pi _ t _) sc)

263+getTCinj i (Bind n (Pi _ _ t _) sc)

264 = getTCinj i t ++ getTCinj i (instantiate (P Bound n t) sc)

265getTCinj i ap@(App _ f a)

266 | (P _ n _, args) <- unApply ap,

@@ -310,14 +310,14 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

310

311 getUniqB env us (Let t v) = getUniq env us v

312 getUniqB env us (Guess t v) = getUniq env us v

313−-- getUniqB env us (Pi t v) = do getUniq env us t; getUniq env us v

313+-- getUniqB env us (Pi _ _ t v) = do getUniq env us t; getUniq env us v

314 getUniqB env us (NLet t v) = getUniq env us v

315 getUniqB env us b = return () -- getUniq env us (binderTy b)

316

317-- In a functional application, return the names which are used

318-- directly in a static position

319getStaticNames :: IState -> Term -> [Name]

320−getStaticNames ist (Bind n (PVar _) sc)

320+getStaticNames ist (Bind n (PVar _ _) sc)

321 = getStaticNames ist (instantiate (P Bound n Erased) sc)

322getStaticNames ist tm

323 | (P _ fn _, args) <- unApply tm

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

331getStaticNames _ _ = []

332

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

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

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

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

336 | otherwise = False : getStatics ns t

337getStatics _ _ = []

@@ -407,7 +407,7 @@ findParams tyn famty ts =

407 getDataApp f@(App _ _ _)

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

409 = if (d == tyn) then [mParam args args] else []

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

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

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

412 getDataApp _ = []

413

@@ -478,9 +478,9 @@ orderPats tm = op [] tm

478 where

479 op [] (App s f a) = App s f (op [] a) -- for Infer terms

480

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

481+ op ps (Bind n (PVar r t) sc) = op ((n, PVar r t) : ps) sc

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

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

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

484 op ps sc = bindAll (sortP ps) sc

485

486 -- Keep explicit Pi in the same order, insert others as necessary,

@@ -488,8 +488,8 @@ orderPats tm = op [] tm

488 sortP ps = let (exps, imps) = partition isExp ps in

489 pick (reverse exps) imps

490

491− isExp (_, Pi Nothing _ _) = True

491+ isExp (_, Pi rig Nothing _ _) = True

492− isExp (_, Pi (Just i) _ _) = toplevel_imp i && not (machine_gen i)

492+ isExp (_, Pi rig (Just i) _ _) = toplevel_imp i && not (machine_gen i)

493 isExp _ = False

494

495 pick acc [] = acc

@@ -510,13 +510,13 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in

510 where

511 bindPats [] tm = tm

512 bindPats ((n, t):ps) tm

513− | n `notElem` map fst ps = Bind n (PVar t) (bindPats ps tm)

513+ | n `notElem` map fst ps = Bind n (PVar RigW t) (bindPats ps tm)

514 | otherwise = bindPats ps tm

515

516 getPats :: Term -> State [(Name, Type)] Term

517− getPats (Bind n (PVar t) sc) = do ps <- get

517+ getPats (Bind n (PVar _ t) sc) = do ps <- get

518− put ((n, t) : ps)

518+ put ((n, t) : ps)

519− getPats sc

519+ getPats sc

520 getPats (Bind n (Guess t v) sc) = do t' <- getPats t

521 v' <- getPats v

522 sc' <- getPats sc

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

525 v' <- getPats v

526 sc' <- getPats sc

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

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

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

529− k' <- getPats k

529+ k' <- getPats k

530− sc' <- getPats sc

530+ sc' <- getPats sc

531− return (Bind n (Pi i t' k') sc')

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

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

533 sc' <- getPats sc

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

@@ -568,6 +568,6 @@ isEmpty ctxt tyctxt ty

568isEmpty ctxt tyinfo ty = False

569

570hasEmptyPat :: Context -> Ctxt TypeInfo -> Term -> Bool

571−hasEmptyPat ctxt tyctxt (Bind n (PVar ty) sc)

571+hasEmptyPat ctxt tyctxt (Bind n (PVar _ ty) sc)

572 = isEmpty ctxt tyctxt ty || hasEmptyPat ctxt tyctxt sc

573hasEmptyPat ctxt tyctxt _ = False

src/Idris/ElabDecls.hs+7−7

@@ -116,9 +116,9 @@ elabPrims = do i <- getIState

116

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

118 p_believeMe _ = Nothing

119− believeTy = Bind (sUN "a") (Pi Nothing (TType (UVar [] (-2))) (TType (UVar [] (-1))))

119+ believeTy = Bind (sUN "a") (Pi RigW Nothing (TType (UVar [] (-2))) (TType (UVar [] (-1))))

120− (Bind (sUN "b") (Pi Nothing (TType (UVar [] (-2))) (TType (UVar [] (-1))))

120+ (Bind (sUN "b") (Pi RigW Nothing (TType (UVar [] (-2))) (TType (UVar [] (-1))))

121− (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar [] (-1)))) (V 1)))

121+ (Bind (sUN "x") (Pi RigW Nothing (V 1) (TType (UVar [] (-1)))) (V 1)))

122 elabBelieveMe

123 = do let prim__believe_me = sUN "prim__believe_me"

124 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

@@ -141,10 +141,10 @@ elabPrims = do i <- getIState

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

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

143

144− synEqTy = Bind (sUN "a") (Pi Nothing (TType (UVar [] (-3))) (TType (UVar [] (-2))))

144+ synEqTy = Bind (sUN "a") (Pi RigW Nothing (TType (UVar [] (-3))) (TType (UVar [] (-2))))

145− (Bind (sUN "b") (Pi Nothing (TType (UVar [] (-3))) (TType (UVar [] (-2))))

145+ (Bind (sUN "b") (Pi RigW Nothing (TType (UVar [] (-3))) (TType (UVar [] (-2))))

146− (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar [] (-2))))

146+ (Bind (sUN "x") (Pi RigW Nothing (V 1) (TType (UVar [] (-2))))

147− (Bind (sUN "y") (Pi Nothing (V 1) (TType (UVar [] (-2))))

147+ (Bind (sUN "y") (Pi RigW Nothing (V 1) (TType (UVar [] (-2))))

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

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

150 elabSynEq

src/Idris/Erasure.hs+1−1

@@ -367,7 +367,7 @@ buildDepMap ci used externs ctx startNames

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

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

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

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

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

371

372 -- let-bound variables can get partially evaluated

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

src/Idris/ErrReverse.hs+1−1

@@ -33,7 +33,7 @@ errReverse ist t = rewrite 5 t -- (elideLambdas t)

33 -- Assume pattern bindings match in l and r (if they don't just treat

34 -- the rule as invalid and return t)

35

36− applyNames ns t (Bind n (PVar ty) scl) (Bind n' (PVar ty') scr)

36+ applyNames ns t (Bind n (PVar _ ty) scl) (Bind n' (PVar _ ty') scr)

37 | n == n' = applyNames (n : ns) t (instantiate (P Ref n ty) scl)

38 (instantiate (P Ref n' ty') scr)

39 | otherwise = t

src/Idris/IBC.hs+1−1

@@ -47,7 +47,7 @@ import System.Directory

47import System.FilePath

48

49ibcVersion :: Word16

50−ibcVersion = 155

50+ibcVersion = 156

51

52-- | When IBC is being loaded - we'll load different things (and omit

53-- different structures/definitions) depending on which phase we're in.

src/Idris/Interactive.hs+8−8

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

390 where getIndent s = length (takeWhile isSpace s)

391

392 appArgs skip 0 _ = ""

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

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

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

395 = " " ++ show n ++ appArgs skip (i - 1) sc

396− appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc

396+ appArgs skip i (Bind _ (Pi _ _ _ _) sc) = appArgs skip (i - 1) sc

397 appArgs skip i _ = ""

398

399 stripMNBind _ args t | args <= 0 = stripImp t

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

416 constraints i [n] ty = showSep ", " (showConstraints i [n] ty) ++ " => "

417 constraints i ns ty = "(" ++ showSep ", " (showConstraints i ns ty) ++ ") => "

418

419− showConstraints i ns (Bind n (Pi _ ty _) sc)

419+ showConstraints i ns (Bind n (Pi _ _ ty _) sc)

420 | n `elem` ns = show (delab i ty) :

421 showConstraints i ns (substV (P Bound n Erased) sc)

422 | otherwise = showConstraints i ns (substV (P Bound n Erased) sc)

@@ -428,9 +428,9 @@ makeLemma fn updatefile l n

428 -- Also, make interface implementations implicit

429 guessImps :: IState -> Context -> Term -> [Name]

430 -- machine names aren't lifted

431− guessImps ist ctxt (Bind n@(MN _ _) (Pi _ ty _) sc)

431+ guessImps ist ctxt (Bind n@(MN _ _) (Pi _ _ ty _) sc)

432 = n : guessImps ist ctxt sc

433− guessImps ist ctxt (Bind n (Pi _ ty _) sc)

433+ guessImps ist ctxt (Bind n (Pi _ _ ty _) sc)

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

435 = n : guessImps ist ctxt sc

436 | isInterface ist ty

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

441 guessImps ist ctxt _ = []

442

443 paramty (TType _) = True

444− paramty (Bind _ (Pi _ (TType _) _) sc) = paramty sc

444+ paramty (Bind _ (Pi _ _ (TType _) _) sc) = paramty sc

445 paramty _ = False

446

447 -- TMP HACK unusable name so don't lift

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

450 _ -> False

451

452 guessInterfaces :: IState -> Context -> [Name] -> [Name] -> Term -> [Name]

453− guessInterfaces ist ctxt binders usednames (Bind n (Pi _ ty _) sc)

453+ guessInterfaces ist ctxt binders usednames (Bind n (Pi _ _ ty _) sc)

454 | isParamInterface ist ty && any (\x -> elem x usednames)

455 (paramNames binders ty)

456 = n : guessInterfaces ist ctxt (n : binders) usednames sc

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

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

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

487-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc

488− guarded ctxt n (Bind _ (Pi _ t _) sc)

488+ guarded ctxt n (Bind _ (Pi _ _ t _) sc)

489 = guarded ctxt n t || guarded ctxt n sc

490 guarded ctxt n _ = False

491

src/Idris/PartialEval.hs+14−14

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

97 where

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

99 -- of expecting it as a function argument

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

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

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

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

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

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

104− st ((ConstraintS, v) : xs) (Bind n (Pi _ t _) sc)

104+ st ((ConstraintS, v) : xs) (Bind n (Pi _ _ t _) sc)

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

106 -- Erase argument from function type

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

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

108 = st xs sc

109 -- Keep types as is

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

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

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

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

112 st _ t = t

113

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

115 -- by substituting the value of previous argument

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

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

117 = do amap <- get

118 case lookup imp amap of

119 Just n' ->

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

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

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

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

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

124 sc' <- unifyEq xs sc

125− return (Bind n (Pi i t k) sc')

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

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

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

127 = do args <- get

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

129 sc' <- unifyEq xs sc

130− return (Bind n (Pi i t k) sc')

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

131 unifyEq xs t = do args <- get

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

133 return t

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

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

142mkPE_TyDecl ist args ty = mkty args ty

143 where

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

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

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

146− mkty ((ConstraintD, v) : xs) (Bind n (Pi _ t k) sc)

146+ mkty ((ConstraintD, v) : xs) (Bind n (Pi rig _ t k) sc)

147 | concreteInterface ist t = mkty xs sc

148 | interfaceConstraint ist t

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

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

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

151 = PPi impl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

152

153 mkty (_ : xs) t

src/Idris/Primitives.hs+1−1

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

32

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

34ty [] x = Constant x

35−ty (t:ts) x = Bind (sMN 0 "T") (Pi Nothing (Constant t) (TType (UVar [] (-3)))) (ty ts x)

35+ty (t:ts) x = Bind (sMN 0 "T") (Pi RigW Nothing (Constant t) (TType (UVar [] (-3)))) (ty ts x)

36

37total, partial, iopartial :: Totality

38total = Total []

src/Idris/ProofSearch.hs+4−4

@@ -346,7 +346,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

346 TermPart ty,

347 TextPart "using proof search, but proof search only works on datatypes with constructors."] ++

348 case ty of

349− (Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]

349+ (Bind _ (Pi _ _ _ _) _) -> [TextPart "In particular, function types are not supported."]

350 _ -> []

351

352-- | Resolve interfaces. This will only pick up 'normal'

@@ -475,9 +475,9 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

475

476 introImps = do g <- goal

477 case g of

478− (Bind _ (Pi _ _ _) sc) -> do attack; intro Nothing

478+ (Bind _ (Pi _ _ _ _) sc) -> do attack; intro Nothing

479− num <- introImps

479+ num <- introImps

480− return (num + 1)

480+ return (num + 1)

481 _ -> return 0

482

483 solven n = replicateM_ n solve

src/Idris/REPL.hs+1−1

@@ -418,7 +418,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

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

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

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

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

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

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

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

424 c, delabTy' ist [] c False False True)

src/Idris/Reflection.hs+8−8

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

316reifyTTBinderApp reif f [t]

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

318reifyTTBinderApp reif f [t, k]

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

319+ | f == reflm "Pi" = liftM2 (Pi RigW Nothing) (reif t) (reif k)

320reifyTTBinderApp reif f [x, y]

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

322reifyTTBinderApp reif f [t]

@@ -326,7 +326,7 @@ reifyTTBinderApp reif f [t]

326reifyTTBinderApp reif f [x, y]

327 | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)

328reifyTTBinderApp reif f [t]

329− | f == reflm "PVar" = liftM PVar (reif t)

329+ | f == reflm "PVar" = liftM (PVar RigW) (reif t)

330reifyTTBinderApp reif f [t]

331 | f == reflm "PVTy" = liftM PVTy (reif t)

332reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))

@@ -582,7 +582,7 @@ reflectBinderQuotePattern q ty unq (Lam t)

582 fill $ reflCall "Lam" [ty, Var t']

583 solve

584 focus t'; q unq t

585−reflectBinderQuotePattern q ty unq (Pi _ t k)

585+reflectBinderQuotePattern q ty unq (Pi _ _ t k)

586 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'

587 k' <- claimTy (sMN 0 "k") ty; movelast k';

588 fill $ reflCall "Pi" [ty, Var t', Var k']

@@ -619,7 +619,7 @@ reflectBinderQuotePattern q ty unq (Guess x y)

619 solve

620 focus x'; q unq x

621 focus y'; q unq y

622−reflectBinderQuotePattern q ty unq (PVar t)

622+reflectBinderQuotePattern q ty unq (PVar _ t)

623 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'

624 fill $ reflCall "PVar" [ty, Var t']

625 solve

@@ -751,7 +751,7 @@ reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []

751reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw

752reflectBinderQuote q ty unq (Lam t)

753 = reflCall "Lam" [Var ty, q unq t]

754−reflectBinderQuote q ty unq (Pi _ t k)

754+reflectBinderQuote q ty unq (Pi _ _ t k)

755 = reflCall "Pi" [Var ty, q unq t, q unq k]

756reflectBinderQuote q ty unq (Let x y)

757 = reflCall "Let" [Var ty, q unq x, q unq y]

@@ -763,7 +763,7 @@ reflectBinderQuote q ty unq (GHole _ _ t)

763 = reflCall "GHole" [Var ty, q unq t]

764reflectBinderQuote q ty unq (Guess x y)

765 = reflCall "Guess" [Var ty, q unq x, q unq y]

766−reflectBinderQuote q ty unq (PVar t)

766+reflectBinderQuote q ty unq (PVar _ t)

767 = reflCall "PVar" [Var ty, q unq t]

768reflectBinderQuote q ty unq (PVTy t)

769 = reflCall "PVTy" [Var ty, q unq t]

@@ -1090,7 +1090,7 @@ reflectList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"

1090-- come from a lookup in idris_implicits on IState.

1091getArgs :: [PArg] -> Raw -> ([RFunArg], Raw)

1092getArgs [] r = ([], r)

1093−getArgs (a:as) (RBind n (Pi _ ty _) sc) =

1093+getArgs (a:as) (RBind n (Pi _ _ ty _) sc) =

1094 let (args, res) = getArgs as sc

1095 erased = if InaccessibleArg `elem` argopts a then RErased else RNotErased

1096 arg' = case a of

@@ -1121,7 +1121,7 @@ buildFunDefns ist n =

1121 mkFunClause ([], lhs, rhs) = RMkFunClause lhs rhs

1122 mkFunClause (((n, ty) : ns), lhs, rhs) = mkFunClause (ns, bind lhs, bind rhs) where

1123 bind Impossible = Impossible

1124− bind tm = Bind n (PVar ty) tm

1124+ bind tm = Bind n (PVar RigW ty) tm

1125

1126-- | Build the reflected datatype definition(s) that correspond(s) to

1127-- a provided unqualified name

src/Idris/Termination.hs+6−6

@@ -112,13 +112,13 @@ checkPositive mut_ns (cn, ty')

112 where

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

114

115− cp i (Bind n (Pi _ aty _) sc)

115+ cp i (Bind n (Pi _ _ aty _) sc)

116 = posArg i aty && cp i sc

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

118 n' `elem` mut_ns = all noRec args

119 cp i _ = True

120

121− posArg ist (Bind _ (Pi _ nty _) sc) = noRec nty && posArg ist sc

121+ posArg ist (Bind _ (Pi _ _ nty _) sc) = noRec nty && posArg ist sc

122 posArg ist t = posParams ist t

123

124 noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)

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

429 = case lookupTy n (tt_ctxt ist) of

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

431 _ -> args

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

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

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

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

434 expand i _ xs = xs

435

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

@@ -476,10 +476,10 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

476 (nty == nty' || any (== nty') muts) && not co

477 isInductive _ _ = False

478

479− dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)

479+ dePat (Bind x (PVar _ ty) sc) = dePat (instantiate (P Bound x ty) sc)

480 dePat t = t

481

482− patvars (Bind x (PVar _) sc) = x : patvars sc

482+ patvars (Bind x (PVar _ _) sc) = x : patvars sc

483 patvars _ = []

484

485 allGuarded n ist = case lookupCtxtExact n (idris_flags ist) of

src/Idris/Transforms.hs+2−2

@@ -86,7 +86,7 @@ applyRule (lhs, rhs) tm

86-- (In general, this would not be true, but when we elaborate transformation

87-- rules we mangle the names so that it is true. While this feels a bit

88-- hacky, it's much easier to think about than mangling de Bruijn indices).

89− where depat ms (Bind n (PVar t) sc)

89+ where depat ms (Bind n (PVar _ t) sc)

90 = case lookup n ms of

91 Just tm -> depat ms (subst n tm sc)

92 _ -> depat ms sc -- no occurrence? Shouldn't happen

@@ -95,7 +95,7 @@ applyRule (lhs, rhs) tm

95matchTerm :: Term -> Term -> Maybe [(Name, Term)]

96matchTerm lhs tm = matchVars [] lhs tm

97 where

98− matchVars acc (Bind n (PVar t) sc) tm

98+ matchVars acc (Bind n (PVar _ t) sc) tm

99 = matchVars (n : acc) (instantiate (P Bound n t) sc) tm

100 matchVars acc sc tm

101 = -- trace (show acc ++ ": " ++ show (sc, tm)) $

src/Idris/TypeSearch.hs+2−2

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

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

143

144 -- NOTE : args are in reverse order

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

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

146 if removePred ty

147 then go args (arg : removedArgs) sc

148 else go (arg : args) removedArgs sc

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

439 unifyQueue state [] = return state

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

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

442− res <- tcToMaybe $ match_unify ctxt [ (n, Rig0, Pi Nothing ty (TType (UVar [] 0))) | (n, ty) <- holes state]

442+ res <- tcToMaybe $ match_unify ctxt [ (n, RigW, Pi RigW Nothing ty (TType (UVar [] 0))) | (n, ty) <- holes state]

443 (ty1, Nothing)

444 (ty2, Nothing) [] (map fst $ holes state) []

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