e1c210b · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+10−10

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

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

14761476 addIBC (IBCStatic n)

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

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

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

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

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

14841484 else if (not (searchArg p))

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

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

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

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

14981498 = n : getParamNames ist sc

14991499 getParamNames ist _ = []

15001500

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

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

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

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

15041504 getNamesFrom i ps sc = []

15051505

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

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

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

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

15091509 concatMap freeNames args

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

15151515 searchArg (TacImp _ _ _) = True

15161516 searchArg _ = False

15171517

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

15191519 staticList _ _ = []

15201520

15211521-- Dealing with implicit arguments

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

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

16241624 scopedimpl _ = False

16251625

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

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

16271627 | scopedimpl i = getImps sc imps

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

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

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

16301630 where

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

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

16411641 argInfo n (TacImp opt _ scr) t'

16421642 = (InaccessibleArg `elem` opt,

16431643 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

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

16461646 getImps sc tm = []

16471647

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

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

21472147 su :: PTerm -> PTerm

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

21502150 = Placeholder

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

21522152 not (implicitable f)

src/Idris/AbsSyntaxTree.hs+2−2

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

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

16201620

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

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

1623− toTy (PVar t) = PVTy t

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

1623+ toTy (PVar _ t) = PVTy t

16241624 toTy b = b

16251625getInferType (App _ (App _ _ ty) _) = ty

16261626

src/Idris/Apropos.hs+1−1

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

7373

7474instance Apropos (Binder (TT Name)) where

7575 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

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

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

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

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

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

214214 _ -> repeat Nothing

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

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

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

217217 d == sUN "Delayed" = tyName ty

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

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

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

490490 return (RUType x1)

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

492492

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+

493506instance Binary ImplicitInfo where

494507 put x

495508 = case x of

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

504517 = case x of

505518 Lam x1 -> do putWord8 0

506519 put x1

507− Pi x1 x2 x3 -> do putWord8 1

508− put x1

509− put x2

510− put x3

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

521+ put x1

522+ put x2

523+ put x3

524+ put x4

511525 Let x1 x2 -> do putWord8 2

512526 put x1

513527 put x2

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

523537 Guess x1 x2 -> do putWord8 6

524538 put x1

525539 put x2

526− PVar x1 -> do putWord8 7

527− put x1

540+ PVar x1 x2 -> do putWord8 7

541+ put x1

542+ put x2

528543 PVTy x1 -> do putWord8 8

529544 put x1

530545 get

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

535550 1 -> do x1 <- get

536551 x2 <- get

537552 x3 <- get

538− return (Pi x1 x2 x3)

553+ x4 <- get

554+ return (Pi x1 x2 x3 x4)

539555 2 -> do x1 <- get

540556 x2 <- get

541557 return (Let x1 x2)

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

552568 x2 <- get

553569 return (Guess x1 x2)

554570 7 -> do x1 <- get

555− return (PVar x1)

571+ x2 <- get

572+ return (PVar x1 x2)

556573 8 -> do x1 <- get

557574 return (PVTy x1)

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

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

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

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

393393 | otherwise = PConst x

394394

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

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

396396 | reflect && noOccurrence n sc

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

398398

src/Idris/Core/DeepSeq.hs+1

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

4040instance NFData Err

4141instance NFData ErrorReportPart

4242instance NFData ImplicitInfo

43+instance NFData RigCount

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

4445instance NFData UExp

4546instance NFData NameType

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

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

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

328328 isInj ctxt (Constant _) = True

329329 isInj ctxt (TType _) = True

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

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

331331 isInj ctxt _ = False

332332

333333-- | get implementation argument names

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

589589 return $! claims

590590 where

591591 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

593593 argsOK _ (i : is) = False

594594 argsOK _ [] = True

595595

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

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

599599 -> [Name] -- ^ Hypotheses

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

602602 do let t = rebind hs t_in

603603 n <- getNameFrom (mkMN n')

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

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

712712 priOrder _ Nothing = GT

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

714714

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

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

716716 do n <- unique_hole (mkMN n')

717717 when (null claims) (start_unify n)

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

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

749749 ctxt <- get_context

750750 env <- get_env

751751 case (whnf ctxt env g) of

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

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

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

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

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

756756 claim a RType

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

759759 movelast a

760760 movelast b

761761 fill (Var f)

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

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

776776 claim a RType

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

779779 tm <- get_term

780780 start_unify s

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

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

826826 case whnf ctxt env fty of

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

828828 -- f's expected argument type

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

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

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

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

832832 _ -> 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

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

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

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

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

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

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

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

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

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

647647

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

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

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

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

652652

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

662662 where

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

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

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

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

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

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

999999 _ -> return ctxt

10001000 return uctxt { definitions = ctxt' }

10011001 where

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

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

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

10041004 depat acc x = (acc, x)

10051005 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

9292 b' <- fixBinder b

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

9494 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

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

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

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

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

100100 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

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

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

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

392392 lift $ isType ctxt env tyt

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

394394 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

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

397397

398398reorder_claims :: RunTactic

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

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

473473 where

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

476476

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

478478defer 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) =

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

542542 -- specific problem.

543543 -- 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 _ _) _))

545545 = TooManyArgs val

546546 chkPurpose _ _ = ExpectedType

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

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

652652 Just name -> name

653653 Nothing -> x

654654 let t' = case t of

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

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

656656 _ -> normalise ctxt env t

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

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

659659 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

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

662662 ps <- get

663663 let (uh, uns) = unified ps

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

669669intro :: Maybe Name -> RunTactic

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

671671 do let t' = case t of

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

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

673673 _ -> normalise ctxt env t

674674 case t' of

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

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

676676 let n = case mn of

677677 Just name -> name

678678 Nothing -> y

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

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

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

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

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

694694

695695patvar :: Name -> RunTactic

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

702702 (notunified ps),

703703 injective = addInj n x (injective ps)

704704 })

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)

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

707707 | otherwise = ps

708708patvar 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' =

830830 _ -> normalise ctxt env t

831831 case t' of

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

834834 _ -> fail "Nothing to pattern bind"

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

836836

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

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

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

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

856856 -- ^ A function binding

857− | Pi { binderImpl :: Maybe ImplicitInfo,

857+ | Pi { binderCount :: RigCount,

858+ binderImpl :: Maybe ImplicitInfo,

858859 binderTy :: !b,

859860 binderKind :: !b }

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

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

886887 -- substituted - the guess is to keep it

887888 -- computationally inert while working on other things

888889 -- if necessary.

889− | PVar { binderTy :: !b }

890+ | PVar { binderCount :: RigCount,

891+ binderTy :: !b }

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

891893 -- that make up pattern-match clauses)

892894 | PVTy { binderTy :: !b }

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

898900

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

900902 size (Lam ty) = 1 + size ty

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

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

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

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

904906 size (Hole ty) = 1 + size ty

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

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

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

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

908910 size (PVTy ty) = 1 + size ty

909911

910912fmapMB :: 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)

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

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

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

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

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

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

920922

921923raw_apply :: Raw -> [Raw] -> Raw

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

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

11281130isInjective (Constant _) = True

11291131isInjective (TType x) = True

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

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

11311133isInjective (App _ f a) = isInjective f

11321134isInjective _ = False

11331135

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

13611363

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

13631365arity :: TT n -> Int

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

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

13651367arity _ = 0

13661368

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

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

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

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

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

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

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

14631465getArgTys _ = []

14641466

14651467getRetTy :: TT n -> TT n

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

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

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

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

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

14691471getRetTy sc = sc

14701472

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

14721474substRetTy :: 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)

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

14761478substRetTy sc = sc

14771479

14781480

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

15891591 else

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

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

15931595 | noOccurrence n sc && not debug =

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

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

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

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

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

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

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

1613− prettySb env n (PVar t) = prettyB env "pat" "." 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

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

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

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

16161621 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

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

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

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

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

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

1641− se p env (Bind n b@(Pi _ 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

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

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

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

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

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

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

1648+ where arrow Rig0 = " -> "

1649+ arrow Rig1 = " -o "

1650+ arrow RigW = " -> "

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

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

16471653 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

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

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

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

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

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

1660− sb env n (PVar t) = showb env "pat " ". " 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

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

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

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

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

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

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

17651774 ppb p bound n (Lam ty) sc =

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

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

17691778 bracket p startPrec . group . align $

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

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

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

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

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

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

1782+ where mkArrow Rig1 = text "⇴"

1783+ mkArrow Rig0 = text "⥛"

17751784 mkArrow _ = text "→"

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

17771786 bracket p startPrec . group . align $

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

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

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

18021811 text "." <> line <> sc

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

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

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

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

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

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

18531862 where

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

18551864 text "Lam" <$> pprintRaw bound ty

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

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

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

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

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

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

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

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

18651874 text "GHole" <$> pprintRaw bound ty

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

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

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

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

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

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

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

18711880 text "PVTy" <$> pprintRaw bound ty

18721881pprintRaw 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

114114 -- special case to reduce constraintss

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

116116 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

118118 _ -> uniqueBinders (map fstEnv env)

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

121121 _ -> normalise ctxt env fty

122122 case fty' of

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

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

124124 do (v, cs) <- get

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

126126 let apty = simplify initContext env

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

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

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

131131 convertsC ctxt env aty s

132132 let apty = simplify initContext env

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

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

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

138138 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

140140 _ -> uniqueBinders (map fstEnv env)

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

143143 _ -> normalise ctxt env fty

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

145145 case fty' of

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

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

147147 do convertsC ctxt env aty s

148148 let apty = simplify initContext env

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

178178 constType TheWorld = Constant WorldType

179179 constType Forgot = Erased

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

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

183183 (v, cs) <- get

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

186186 let maxu = case lvl of

187187 Nothing -> UVar tcns v

188188 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

191190

192191-- convertsC ctxt env st (TType maxu)

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

201200 put (v, ULE su maxu :

202201 ULE tu maxu : cs)

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

205204 (pToV n tv), k')

206205 (un, un') ->

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

209208 (pToV n tv), k')

210209

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

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

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

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

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

216215 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

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

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

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

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

225224

226225 chk u lvl env (RBind n b sc)

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

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

231− where checkBinder (Lam t)

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

230+ getCount (PVar rig _) = rig

231+ getCount _ = Rig0

232+

233+ checkBinder (Lam t)

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

233235 let tv' = normalise ctxt env tv

234236 convType tcns ctxt env tt

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

268270 convertsC ctxt env vt tv

269271 convType tcns ctxt env tt

270272 return (Guess tv vv, tt)

271− checkBinder (PVar t)

273+ checkBinder (PVar rig t)

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

273275 let tv' = normalise ctxt env tv

274276 convType tcns ctxt env tt

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

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

277− return (PVar tv, tt)

279+ return (PVar rig tv, tt)

278280 checkBinder (PVTy t)

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

280282 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

282284 return (PVTy tv, tt)

283285

284286 discharge n (Lam t) bt scv sct

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

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

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

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

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

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

288290 discharge n (Let t v) bt scv sct

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

290292 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

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

296298 discharge n (Guess t v) bt scv sct

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

298− discharge n (PVar t) bt scv sct

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

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

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

300302 discharge n (PVTy t) bt scv sct

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

302304

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

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

141141 h2 <- un bnames vx vy

142142 combine bnames h1 h2

143143 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

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

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

147147 (normalise ctxt env (binderTy y))

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

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

492492 -- interface resolution for interfaces over functions.

493493

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)

495495 | noOccurrence n y && injectiveApp f

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

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

499499 combine env bnames ux uf

500500

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)

502502 | noOccurrence n y && injectiveApp f

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

504504 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

506506 combine env bnames ux uf

507507

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

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

512512 combine env bnames h1 h2

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

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

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

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

516516 un' env fn bnames x y

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

643643 sc 1

644644 combine env bnames h1 h2

645645 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

647647 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

649649 uB env bnames x y

650650 = do UI s f <- get

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

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

754754 | f == f' = recoverable a a'

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

756756 = recoverable f f' -- && recoverable a a'

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

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

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

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

760760 | (Constant _) <- f = False

761761 | TType _ <- f = False

762762 | UType _ <- f = False

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

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

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

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

766766 | (Constant _) <- f = False

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

781781

782782patIn :: Env -> Name -> Bool

783783patIn env n = case lookupBinder n env of

784− Just (PVar _) -> True

784+ Just (PVar _ _) -> True

785785 Just (PVTy _) -> True

786786 _ -> False

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

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

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

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

7474 -- the name

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

76− -- TODO: Get RigCount from Pi

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

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

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

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

7978 res -> tm

8079

src/Idris/Delaborate.hs+9−9

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

137137 _ -> PRef un [] n

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

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

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

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

144144 | tcimplementation impl

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

146146 | otherwise

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

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

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

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

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

156156 n NoFC

157157 (de env [] ty)

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

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

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

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

161161

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

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

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

340340 y)) <>

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

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

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

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

347347 flagUnique t = t

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

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

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

330330 (vs, x', Impossible)

331331

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)

333333 depat acc x = (acc, x)

334334

335335

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

337− in (x:vs, tm')

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

337+ in (x:vs, tm')

338338 getPVs tm = ([], tm)

339339

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

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

529529 _ -> True

530530 concreteTm ist (Constant _) = True

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

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

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

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

534534 concreteTm ist _ = False

535535

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

11061106 let wargname = sMN windex "warg"

11071107

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

11101110 (wargname, wargtype) :

11111111 map (abstract wargname wargval wargtype) bargs_post ++

11121112 case mpn of

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

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

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

12021202 where

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

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

12041204 getImps _ = []

12051205

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

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

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

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

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

13041304 getTm a == Placeholder

13051305 = case lookupCtxtExact cn (idris_interfaces ist) of

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

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

13091309 = a : addResolvesArgs fc sc args

13101310 addResolvesArgs fc _ args = args

13111311

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

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

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

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

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

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

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

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

272272 forceFrom i sc

273273 -- Go under the top level type application

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

310310 where

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

312312

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

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

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

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

316316 = paramArgs 0 args

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

321321

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

323323 where

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

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

325325 = case getRetTy ty of

326326 TType avar -> do tit <- typeInType

327327 when (not tit) $ do

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

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

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

517517 isInj _ _ = True

518518

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

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

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

521521 instantiateRetTy t = t

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

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

376376 Just ty -> getDetPos 0 ns ty

377377 Nothing -> []

378378 where

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

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

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

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

382382 getDetPos _ _ _ = []

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

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

156156

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

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

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

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

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

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

165165getParamInfo _ _ _ _ = []

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

249249 mkArgs _ _ _ = []

250250

251251 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

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

255255 = PPi forall_imp i fc (delab ist ty)

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

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

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

261261 bindIdxs _ _ _ _ tm = tm

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

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

201201 Nothing -> []

202202 Just ty -> checkArgs [] [] ty

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

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

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

205205 = let env' = case t of

206206 TType _ -> n : env

207207 _ -> env in

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

810810 ans <- claimArgTys env xs

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

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

814814

815815 localVar env (PRef _ _ x)

816816 = case lookupBinder x env of

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

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

958958 checkKnownImplicit _ = return ()

959959

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

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

961961 = i : getReqImps sc

962962 getReqImps _ = []

963963

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

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

14851485 fullApp x = x

14861486

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

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

14881488 | tcimplementation i && not (toplevel_imp i)

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

14901490 | not (toplevel_imp i)

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

14931493 = x : insertScopedImps fc sc xs

14941494 insertScopedImps _ _ xs = xs

14951495

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

15001500 addLam ty' t

15011501 where

15021502 -- just one level at a time

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

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

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

15051505 if e_isfn ina -- apply to an implicit immediately

15061506 then return (PApp emptyFC

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

17821782 where

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

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

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

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

17861786 = let tcs' = case unApply ty of

17871787 (P _ c _, _) ->

17881788 case lookupCtxtExact c (idris_interfaces ist) of

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

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

19171917

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

19201920 patvars ns tm = (ns, tm)

19211921

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

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

19851985

19861986 -- | Add another argument to a Pi

19871987 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

19891989

19901990 mustBeType ctxt tm ty =

19911991 case normaliseAll ctxt [] (finalise ty) of

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

20422042 _ -> n

20432043

20442044 getRetTy :: Type -> Type

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

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

20462046 getRetTy ty = ty

20472047

20482048 elabScriptStuck :: Term -> ElabD a

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

26172617 where tacticTy = Var (reflm "Tactic")

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

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

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

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

26212621 (RBind (sMN 1 "__pi_arg")

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

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

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

26242624 -- goal, then apply the resulting reflected Tactic

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

114114 return (clhs_tm, crhs_tm)

115115

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

118118 depat x = x

119119

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

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

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

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

122122 renamepats _ sc = sc

123123

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

135135

136136 return (cty, ckind, ty, inacc)

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

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

140140 patToImp t = t

141141

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

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

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

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

145145 param_pos i ns t = []

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

260260 lst = txt "List"

261261 errrep = txt "ErrorReportPart"

262262

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

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

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

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

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

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

104104-- type

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

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

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

109109inaccessibleImps _ _ _ = []

@@ -184,7 +184,7 @@ decorateid decorate (PClauses f o n cs)

184184

185185-- if 't' is an interface application, assume its arguments are injective

186186pbinds :: IState -> Term -> ElabD ()

187−pbinds i (Bind n (PVar t) sc)

187+pbinds i (Bind n (PVar _ t) sc)

188188 = do attack; patbind n

189189 env <- get_env

190190 case unApply (normalise (tt_ctxt i) env t) of

@@ -198,26 +198,26 @@ pbinds i (Bind n (PVar t) sc)

198198 setinjArg _ = return ()

199199pbinds i tm = return ()

200200

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)

202202pbty _ tm = tm

203203

204−getPBtys (Bind n (PVar t) sc) = (n, t) : getPBtys sc

204+getPBtys (Bind n (PVar _ t) sc) = (n, t) : getPBtys sc

205205getPBtys (Bind n (PVTy t) sc) = (n, t) : getPBtys sc

206206getPBtys _ = []

207207

208−psolve (Bind n (PVar t) sc) = do solve; psolve sc

208+psolve (Bind n (PVar _ t) sc) = do solve; psolve sc

209209psolve tm = return ()

210210

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

212212pvars ist _ = []

213213

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

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

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

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

217217 ++ case unApply t of

218218 (P _ n _, _) -> if n `elem` env then [n] else []

219219 _ -> []

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

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

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

222222getFixedInType i env is tm@(App _ f a)

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

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

231231 getFixedInType i env is a

232232getFixedInType i _ _ _ = []

233233

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

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

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

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

237237

@@ -260,7 +260,7 @@ getParamsInType i env ps t = let fix = getFixedInType i env ps t

260260 flex = getFlexInType i env fix t in

261261 [x | x <- fix, not (x `elem` flex)]

262262

263−getTCinj i (Bind n (Pi _ t _) sc)

263+getTCinj i (Bind n (Pi _ _ t _) sc)

264264 = getTCinj i t ++ getTCinj i (instantiate (P Bound n t) sc)

265265getTCinj i ap@(App _ f a)

266266 | (P _ n _, args) <- unApply ap,

@@ -310,14 +310,14 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

310310

311311 getUniqB env us (Let t v) = getUniq env us v

312312 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

314314 getUniqB env us (NLet t v) = getUniq env us v

315315 getUniqB env us b = return () -- getUniq env us (binderTy b)

316316

317317-- In a functional application, return the names which are used

318318-- directly in a static position

319319getStaticNames :: IState -> Term -> [Name]

320−getStaticNames ist (Bind n (PVar _) sc)

320+getStaticNames ist (Bind n (PVar _ _) sc)

321321 = getStaticNames ist (instantiate (P Bound n Erased) sc)

322322getStaticNames ist tm

323323 | (P _ fn _, args) <- unApply tm

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

331331getStaticNames _ _ = []

332332

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

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

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

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

336336 | otherwise = False : getStatics ns t

337337getStatics _ _ = []

@@ -407,7 +407,7 @@ findParams tyn famty ts =

407407 getDataApp f@(App _ _ _)

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

409409 = if (d == tyn) then [mParam args args] else []

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

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

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

412412 getDataApp _ = []

413413

@@ -478,9 +478,9 @@ orderPats tm = op [] tm

478478 where

479479 op [] (App s f a) = App s f (op [] a) -- for Infer terms

480480

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

482482 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

484484 op ps sc = bindAll (sortP ps) sc

485485

486486 -- Keep explicit Pi in the same order, insert others as necessary,

@@ -488,8 +488,8 @@ orderPats tm = op [] tm

488488 sortP ps = let (exps, imps) = partition isExp ps in

489489 pick (reverse exps) imps

490490

491− isExp (_, Pi Nothing _ _) = True

492− isExp (_, Pi (Just i) _ _) = toplevel_imp i && not (machine_gen i)

491+ isExp (_, Pi rig Nothing _ _) = True

492+ isExp (_, Pi rig (Just i) _ _) = toplevel_imp i && not (machine_gen i)

493493 isExp _ = False

494494

495495 pick acc [] = acc

@@ -510,13 +510,13 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in

510510 where

511511 bindPats [] tm = tm

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

514514 | otherwise = bindPats ps tm

515515

516516 getPats :: Term -> State [(Name, Type)] Term

517− getPats (Bind n (PVar t) sc) = do ps <- get

518− put ((n, t) : ps)

519− getPats sc

517+ getPats (Bind n (PVar _ t) sc) = do ps <- get

518+ put ((n, t) : ps)

519+ getPats sc

520520 getPats (Bind n (Guess t v) sc) = do t' <- getPats t

521521 v' <- getPats v

522522 sc' <- getPats sc

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

525525 v' <- getPats v

526526 sc' <- getPats sc

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

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

529− k' <- getPats k

530− sc' <- getPats sc

531− return (Bind n (Pi i t' k') sc')

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

529+ k' <- getPats k

530+ sc' <- getPats sc

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

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

533533 sc' <- getPats sc

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

@@ -568,6 +568,6 @@ isEmpty ctxt tyctxt ty

568568isEmpty ctxt tyinfo ty = False

569569

570570hasEmptyPat :: Context -> Ctxt TypeInfo -> Term -> Bool

571−hasEmptyPat ctxt tyctxt (Bind n (PVar ty) sc)

571+hasEmptyPat ctxt tyctxt (Bind n (PVar _ ty) sc)

572572 = isEmpty ctxt tyctxt ty || hasEmptyPat ctxt tyctxt sc

573573hasEmptyPat ctxt tyctxt _ = False

src/Idris/ElabDecls.hs+7−7

@@ -116,9 +116,9 @@ elabPrims = do i <- getIState

116116

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

118118 p_believeMe _ = Nothing

119− believeTy = Bind (sUN "a") (Pi Nothing (TType (UVar [] (-2))) (TType (UVar [] (-1))))

120− (Bind (sUN "b") (Pi Nothing (TType (UVar [] (-2))) (TType (UVar [] (-1))))

121− (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar [] (-1)))) (V 1)))

119+ believeTy = Bind (sUN "a") (Pi RigW 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 RigW Nothing (V 1) (TType (UVar [] (-1)))) (V 1)))

122122 elabBelieveMe

123123 = do let prim__believe_me = sUN "prim__believe_me"

124124 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

@@ -141,10 +141,10 @@ elabPrims = do i <- getIState

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

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

143143

144− synEqTy = Bind (sUN "a") (Pi Nothing (TType (UVar [] (-3))) (TType (UVar [] (-2))))

145− (Bind (sUN "b") (Pi Nothing (TType (UVar [] (-3))) (TType (UVar [] (-2))))

146− (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar [] (-2))))

147− (Bind (sUN "y") (Pi Nothing (V 1) (TType (UVar [] (-2))))

144+ synEqTy = Bind (sUN "a") (Pi RigW 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 RigW Nothing (V 1) (TType (UVar [] (-2))))

147+ (Bind (sUN "y") (Pi RigW Nothing (V 1) (TType (UVar [] (-2))))

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

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

150150 elabSynEq

src/Idris/Erasure.hs+1−1

@@ -367,7 +367,7 @@ buildDepMap ci used externs ctx startNames

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

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

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

371371

372372 -- let-bound variables can get partially evaluated

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

3333 -- Assume pattern bindings match in l and r (if they don't just treat

3434 -- the rule as invalid and return t)

3535

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)

3737 | n == n' = applyNames (n : ns) t (instantiate (P Ref n ty) scl)

3838 (instantiate (P Ref n' ty') scr)

3939 | otherwise = t

src/Idris/IBC.hs+1−1

@@ -47,7 +47,7 @@ import System.Directory

4747import System.FilePath

4848

4949ibcVersion :: Word16

50−ibcVersion = 155

50+ibcVersion = 156

5151

5252-- | When IBC is being loaded - we'll load different things (and omit

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

390390 where getIndent s = length (takeWhile isSpace s)

391391

392392 appArgs skip 0 _ = ""

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

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

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

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

397397 appArgs skip i _ = ""

398398

399399 stripMNBind _ args t | args <= 0 = stripImp t

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

416416 constraints i [n] ty = showSep ", " (showConstraints i [n] ty) ++ " => "

417417 constraints i ns ty = "(" ++ showSep ", " (showConstraints i ns ty) ++ ") => "

418418

419− showConstraints i ns (Bind n (Pi _ ty _) sc)

419+ showConstraints i ns (Bind n (Pi _ _ ty _) sc)

420420 | n `elem` ns = show (delab i ty) :

421421 showConstraints i ns (substV (P Bound n Erased) sc)

422422 | otherwise = showConstraints i ns (substV (P Bound n Erased) sc)

@@ -428,9 +428,9 @@ makeLemma fn updatefile l n

428428 -- Also, make interface implementations implicit

429429 guessImps :: IState -> Context -> Term -> [Name]

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

432432 = n : guessImps ist ctxt sc

433− guessImps ist ctxt (Bind n (Pi _ ty _) sc)

433+ guessImps ist ctxt (Bind n (Pi _ _ ty _) sc)

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

435435 = n : guessImps ist ctxt sc

436436 | isInterface ist ty

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

441441 guessImps ist ctxt _ = []

442442

443443 paramty (TType _) = True

444− paramty (Bind _ (Pi _ (TType _) _) sc) = paramty sc

444+ paramty (Bind _ (Pi _ _ (TType _) _) sc) = paramty sc

445445 paramty _ = False

446446

447447 -- TMP HACK unusable name so don't lift

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

450450 _ -> False

451451

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

454454 | isParamInterface ist ty && any (\x -> elem x usednames)

455455 (paramNames binders ty)

456456 = n : guessInterfaces ist ctxt (n : binders) usednames sc

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

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

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

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

489489 = guarded ctxt n t || guarded ctxt n sc

490490 guarded ctxt n _ = False

491491

src/Idris/PartialEval.hs+14−14

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

9797 where

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

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

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

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

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

106106 -- Erase argument from function type

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

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

108108 = st xs sc

109109 -- Keep types as is

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

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

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

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

112112 st _ t = t

113113

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

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

117117 = do amap <- get

118118 case lookup imp amap of

119119 Just n' ->

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

121121 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

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

124124 sc' <- unifyEq xs sc

125− return (Bind n (Pi i t k) sc')

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

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

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

127127 = do args <- get

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

129129 sc' <- unifyEq xs sc

130− return (Bind n (Pi i t k) sc')

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

131131 unifyEq xs t = do args <- get

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

133133 return t

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

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

142142mkPE_TyDecl ist args ty = mkty args ty

143143 where

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

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

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

147147 | concreteInterface ist t = mkty xs sc

148148 | interfaceConstraint ist t

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

151151 = PPi impl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

152152

153153 mkty (_ : xs) t

src/Idris/Primitives.hs+1−1

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

3232

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

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

3636

3737total, partial, iopartial :: Totality

3838total = Total []

src/Idris/ProofSearch.hs+4−4

@@ -346,7 +346,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

346346 TermPart ty,

347347 TextPart "using proof search, but proof search only works on datatypes with constructors."] ++

348348 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."]

350350 _ -> []

351351

352352-- | Resolve interfaces. This will only pick up 'normal'

@@ -475,9 +475,9 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

475475

476476 introImps = do g <- goal

477477 case g of

478− (Bind _ (Pi _ _ _) sc) -> do attack; intro Nothing

479− num <- introImps

480− return (num + 1)

478+ (Bind _ (Pi _ _ _ _) sc) -> do attack; intro Nothing

479+ num <- introImps

480+ return (num + 1)

481481 _ -> return 0

482482

483483 solven n = replicateM_ n solve

src/Idris/REPL.hs+1−1

@@ -418,7 +418,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

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

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

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

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

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

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

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

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

316316reifyTTBinderApp reif f [t]

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

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

320320reifyTTBinderApp reif f [x, y]

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

322322reifyTTBinderApp reif f [t]

@@ -326,7 +326,7 @@ reifyTTBinderApp reif f [t]

326326reifyTTBinderApp reif f [x, y]

327327 | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)

328328reifyTTBinderApp reif f [t]

329− | f == reflm "PVar" = liftM PVar (reif t)

329+ | f == reflm "PVar" = liftM (PVar RigW) (reif t)

330330reifyTTBinderApp reif f [t]

331331 | f == reflm "PVTy" = liftM PVTy (reif t)

332332reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))

@@ -582,7 +582,7 @@ reflectBinderQuotePattern q ty unq (Lam t)

582582 fill $ reflCall "Lam" [ty, Var t']

583583 solve

584584 focus t'; q unq t

585−reflectBinderQuotePattern q ty unq (Pi _ t k)

585+reflectBinderQuotePattern q ty unq (Pi _ _ t k)

586586 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'

587587 k' <- claimTy (sMN 0 "k") ty; movelast k';

588588 fill $ reflCall "Pi" [ty, Var t', Var k']

@@ -619,7 +619,7 @@ reflectBinderQuotePattern q ty unq (Guess x y)

619619 solve

620620 focus x'; q unq x

621621 focus y'; q unq y

622−reflectBinderQuotePattern q ty unq (PVar t)

622+reflectBinderQuotePattern q ty unq (PVar _ t)

623623 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'

624624 fill $ reflCall "PVar" [ty, Var t']

625625 solve

@@ -751,7 +751,7 @@ reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []

751751reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw

752752reflectBinderQuote q ty unq (Lam t)

753753 = reflCall "Lam" [Var ty, q unq t]

754−reflectBinderQuote q ty unq (Pi _ t k)

754+reflectBinderQuote q ty unq (Pi _ _ t k)

755755 = reflCall "Pi" [Var ty, q unq t, q unq k]

756756reflectBinderQuote q ty unq (Let x y)

757757 = reflCall "Let" [Var ty, q unq x, q unq y]

@@ -763,7 +763,7 @@ reflectBinderQuote q ty unq (GHole _ _ t)

763763 = reflCall "GHole" [Var ty, q unq t]

764764reflectBinderQuote q ty unq (Guess x y)

765765 = reflCall "Guess" [Var ty, q unq x, q unq y]

766−reflectBinderQuote q ty unq (PVar t)

766+reflectBinderQuote q ty unq (PVar _ t)

767767 = reflCall "PVar" [Var ty, q unq t]

768768reflectBinderQuote q ty unq (PVTy t)

769769 = reflCall "PVTy" [Var ty, q unq t]

@@ -1090,7 +1090,7 @@ reflectList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"

10901090-- come from a lookup in idris_implicits on IState.

10911091getArgs :: [PArg] -> Raw -> ([RFunArg], Raw)

10921092getArgs [] r = ([], r)

1093−getArgs (a:as) (RBind n (Pi _ ty _) sc) =

1093+getArgs (a:as) (RBind n (Pi _ _ ty _) sc) =

10941094 let (args, res) = getArgs as sc

10951095 erased = if InaccessibleArg `elem` argopts a then RErased else RNotErased

10961096 arg' = case a of

@@ -1121,7 +1121,7 @@ buildFunDefns ist n =

11211121 mkFunClause ([], lhs, rhs) = RMkFunClause lhs rhs

11221122 mkFunClause (((n, ty) : ns), lhs, rhs) = mkFunClause (ns, bind lhs, bind rhs) where

11231123 bind Impossible = Impossible

1124− bind tm = Bind n (PVar ty) tm

1124+ bind tm = Bind n (PVar RigW ty) tm

11251125

11261126-- | Build the reflected datatype definition(s) that correspond(s) to

11271127-- a provided unqualified name

src/Idris/Termination.hs+6−6

@@ -112,13 +112,13 @@ checkPositive mut_ns (cn, ty')

112112 where

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

114114

115− cp i (Bind n (Pi _ aty _) sc)

115+ cp i (Bind n (Pi _ _ aty _) sc)

116116 = posArg i aty && cp i sc

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

118118 n' `elem` mut_ns = all noRec args

119119 cp i _ = True

120120

121− posArg ist (Bind _ (Pi _ nty _) sc) = noRec nty && posArg ist sc

121+ posArg ist (Bind _ (Pi _ _ nty _) sc) = noRec nty && posArg ist sc

122122 posArg ist t = posParams ist t

123123

124124 noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)

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

429429 = case lookupTy n (tt_ctxt ist) of

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

431431 _ -> args

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

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

434434 expand i _ xs = xs

435435

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

@@ -476,10 +476,10 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

476476 (nty == nty' || any (== nty') muts) && not co

477477 isInductive _ _ = False

478478

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)

480480 dePat t = t

481481

482− patvars (Bind x (PVar _) sc) = x : patvars sc

482+ patvars (Bind x (PVar _ _) sc) = x : patvars sc

483483 patvars _ = []

484484

485485 allGuarded n ist = case lookupCtxtExact n (idris_flags ist) of

src/Idris/Transforms.hs+2−2

@@ -86,7 +86,7 @@ applyRule (lhs, rhs) tm

8686-- (In general, this would not be true, but when we elaborate transformation

8787-- rules we mangle the names so that it is true. While this feels a bit

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

9090 = case lookup n ms of

9191 Just tm -> depat ms (subst n tm sc)

9292 _ -> depat ms sc -- no occurrence? Shouldn't happen

@@ -95,7 +95,7 @@ applyRule (lhs, rhs) tm

9595matchTerm :: Term -> Term -> Maybe [(Name, Term)]

9696matchTerm lhs tm = matchVars [] lhs tm

9797 where

98− matchVars acc (Bind n (PVar t) sc) tm

98+ matchVars acc (Bind n (PVar _ t) sc) tm

9999 = matchVars (n : acc) (instantiate (P Bound n t) sc) tm

100100 matchVars acc sc tm

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

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

143143

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

146146 if removePred ty

147147 then go args (arg : removedArgs) sc

148148 else go (arg : args) removedArgs sc

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

439439 unifyQueue state [] = return state

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

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

443443 (ty1, Nothing)

444444 (ty2, Nothing) [] (map fst $ holes state) []

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