{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE PatternSynonyms     #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | The judgements — @typecheck@ and @infer@ — and the hole inventory.
--
-- The two belong together: checking a hole records its goal and context, and
-- recording a hole probes what could fill it, which typechecks and unifies
-- candidate terms.
module Rzk.TypeCheck.Judgements where

import           Control.Applicative      ((<|>))
import           Control.Monad            (forM, forM_, unless, when)
import           Control.Monad.Except     (catchError)
import           Control.Monad.Reader     (ask, asks, local)
import           Data.List                (intercalate, sortOn, tails)
import qualified Data.IntMap              as IntMap
import qualified Data.IntSet              as IntSet
import           Data.Bifunctor           (bimap)
import qualified Data.Map                 as Map
import qualified Data.Set                 as Set
import           Data.Maybe               (fromMaybe, isNothing)
import           Data.String              (fromString)
import qualified Data.Text                as T

import           Control.Monad.Foil       (Distinct)
import qualified Control.Monad.Foil       as Foil
import           Control.Monad.Foil.Internal (NameMap (..))
import           Control.Monad.Free.Foil  (AST (Node, Var), ScopedAST (..),
                                           alphaEquiv)

import qualified Language.Rzk.Foil.Convert as Convert
import           Language.Rzk.Foil.Syntax
import           Language.Rzk.Foil.Names (Binder (..), TModality (..),
                                           TypeInfo (..), VarIdent,
                                           binderDisplayName, binderIsCompound,
                                           binderLeaves, binderName,
                                           binderToPattern,
                                           freshenBinderLeavesIn, getVarIdent,
                                           markUnresolved, refreshVarIn,
                                           ppVarIdentWithLocation,
                                           unmarkUnresolved)
import qualified Language.Rzk.Syntax      as Rzk
import           Rzk.TypeCheck.Context
import           Rzk.TypeCheck.Display
import           Rzk.TypeCheck.Error
import           Rzk.TypeCheck.Eval
import           Rzk.TypeCheck.Monad
import           Rzk.TypeCheck.Render
import           Rzk.TypeCheck.Unify

-- * Layers of a goal

isCubeType :: TermT n -> Bool
isCubeType :: forall (n :: S). TermT n -> Bool
isCubeType = \case
  CubeUnitT{}     -> Bool
True
  Cube2T{}        -> Bool
True
  CubeIT{}        -> Bool
True
  CubeProductT{}  -> Bool
True
  UniverseCubeT{} -> Bool
True
  TermT n
_               -> Bool
False

-- | Is a (WHNF) goal type in the cube or tope layer, so that a hole of this type
-- is a cube point or a tope rather than a term? Used to suppress the
-- type-layer-specific hole candidates (@recOR@, @recBOT@), which cannot inhabit a
-- cube or a tope.
isCubeOrTopeType :: TermT n -> Bool
isCubeOrTopeType :: forall (n :: S). TermT n -> Bool
isCubeOrTopeType TermT n
t = TermT n -> Bool
forall (n :: S). TermT n -> Bool
isCubeType TermT n
t Bool -> Bool -> Bool
|| case TermT n
t of
  UniverseTopeT{} -> Bool
True
  TermT n
_               -> Bool
False

-- * Shadowing

-- | The names in scope a new one would shadow.
doesShadowName :: VarIdent -> TypeCheck n [VarIdent]
doesShadowName :: forall (n :: S). VarIdent -> TypeCheck n [VarIdent]
doesShadowName VarIdent
name = (Context n -> [VarIdent])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [VarIdent]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (VarIdent -> Context n -> [VarIdent]
forall (n :: S). VarIdent -> Context n -> [VarIdent]
shadowedBy VarIdent
name)

checkTopLevelDuplicate :: Distinct n => VarIdent -> TypeCheck n ()
checkTopLevelDuplicate :: forall (n :: S). Distinct n => VarIdent -> TypeCheck n ()
checkTopLevelDuplicate VarIdent
name =
  VarIdent -> TypeCheck n [VarIdent]
forall (n :: S). VarIdent -> TypeCheck n [VarIdent]
doesShadowName VarIdent
name TypeCheck n [VarIdent]
-> ([VarIdent]
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    []         -> ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    [VarIdent]
collisions -> TypeError n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> TypeError n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a b. (a -> b) -> a -> b
$ [VarIdent] -> VarIdent -> TypeError n
forall (n :: S). [VarIdent] -> VarIdent -> TypeError n
TypeErrorDuplicateTopLevel [VarIdent]
collisions VarIdent
name

checkNameShadowing :: VarIdent -> TypeCheck n ()
checkNameShadowing :: forall (n :: S). VarIdent -> TypeCheck n ()
checkNameShadowing VarIdent
name =
  VarIdent -> TypeCheck n [VarIdent]
forall (n :: S). VarIdent -> TypeCheck n [VarIdent]
doesShadowName VarIdent
name TypeCheck n [VarIdent]
-> ([VarIdent]
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    [] -> ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    [VarIdent]
collisions -> String
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S). String -> TypeCheck n ()
issueWarning (String
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> String
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a b. (a -> b) -> a -> b
$
      VarIdent' RzkPosition -> String
forall a. Print a => a -> String
Rzk.printTree (VarIdent -> VarIdent' RzkPosition
getVarIdent VarIdent
name) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" shadows an existing definition:"
      String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [String] -> String
unlines
        [ String
"  " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> VarIdent -> String
ppVarIdentWithLocation VarIdent
name
        , String
"previous top-level definitions found at"
        , String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n"
          [ String
"  " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> VarIdent -> String
ppVarIdentWithLocation VarIdent
prev | VarIdent
prev <- [VarIdent]
collisions ] ]

-- * The hole inventory

-- | A fresh hole of the given type.
mkHole :: TermT n -> TermT n
mkHole :: forall (n :: S). TermT n -> TermT n
mkHole = Maybe VarIdent -> TermT n -> TermT n
forall (n :: S). Maybe VarIdent -> TermT n -> TermT n
mkNamedHole Maybe VarIdent
forall a. Maybe a
Nothing

-- | A hole carrying a name, so a suggested move can say what each of its holes
-- stands for: @id-hom ?A ?x@ rather than @id-hom ? ?@. The name is the Π
-- binder's, so the move reads like the lemma's own signature, and two spines of
-- the same lemma applied to different numbers of arguments are told apart by
-- what the extra holes are called.
mkNamedHole :: Maybe VarIdent -> TermT n -> TermT n
mkNamedHole :: forall (n :: S). Maybe VarIdent -> TermT n -> TermT n
mkNamedHole Maybe VarIdent
mname TermT n
t =
  TypeInfo (TermT n) -> Maybe VarIdent -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Maybe VarIdent -> AST binder (AnnSig ann TermSig) n
HoleT TypeInfo{ infoType :: TermT n
infoType = TermT n
t, infoWHNF :: Maybe (TermT n)
infoWHNF = Maybe (TermT n)
forall a. Maybe a
Nothing, infoNF :: Maybe (TermT n)
infoNF = Maybe (TermT n)
forall a. Maybe a
Nothing } Maybe VarIdent
mname

-- | The constructors of a @#data@ type former, in declaration order; empty
-- for anything else. Found by their roles: the type former itself carries
-- none, so the scan is over the names in scope.
dataConstructorsOf :: Foil.Name n -> TypeCheck n [Foil.Name n]
dataConstructorsOf :: forall (n :: S). Name n -> TypeCheck n [Name n]
dataConstructorsOf Name n
d = do
  ctx <- ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Context n)
forall r (m :: * -> *). MonadReader r m => m r
ask
  pure $ map snd $ sortOn fst
    [ (idx, v)
    | v <- ctxBound ctx
    , Just (DataRole d' _ (DataConKind _ idx _ _)) <- [varDataRole (lookupVarInfo v ctx)]
    , Foil.nameId d' == Foil.nameId d
    ]

-- | The generated eliminators of a @#data@ type former (@ind-D@ before
-- @rec-D@), with their roles.
dataEliminatorsOf :: Foil.Name n -> TypeCheck n [(Foil.Name n, DataRole n)]
dataEliminatorsOf :: forall (n :: S). Name n -> TypeCheck n [(Name n, DataRole n)]
dataEliminatorsOf Name n
d = do
  ctx <- ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Context n)
forall r (m :: * -> *). MonadReader r m => m r
ask
  pure $ map snd $ sortOn fst
    [ (order, (v, role))
    | v <- ctxBound ctx
    , Just role@(DataRole d' _ (DataElimKind _ _ elimKind)) <-
        [varDataRole (lookupVarInfo v ctx)]
    , Foil.nameId d' == Foil.nameId d
    , let order = case ElimKind
elimKind of ElimKind
ElimInd -> Int
0 :: Int; ElimKind
ElimRec -> Int
1
    ]

-- | A term of the given type built as λ-binders over a single typed hole
-- (structurally: the motive types the generator builds are literal
-- Π-chains). The eliminators pass such a motive so that their result type
-- β-reduces to the hole and fits any goal, exactly like @idJ@'s motive.
lambdaHoleOf :: Distinct n => Set.Set VarIdent -> Foil.Scope n -> TermT n -> TermT n
lambdaHoleOf :: forall (n :: S).
Distinct n =>
Set VarIdent -> Scope n -> TermT n -> TermT n
lambdaHoleOf Set VarIdent
taken Scope n
scope TermT n
ty = case TermT n
ty of
  TypeFunT TypeInfo (TermT n)
_info Binder
orig TModality
_md TermT n
_param Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret ->
    Scope n
-> (forall (l :: S). DExt n l => NameBinder n l -> TermT n)
-> TermT n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall (l :: S). DExt n l => NameBinder n l -> TermT n)
 -> TermT n)
-> (forall (l :: S). DExt n l => NameBinder n l -> TermT n)
-> TermT n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
b ->
      let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
b Scope n
scope
          retAt :: AST NameBinder (AnnSig TypeInfo TermSig) l
retAt = Scope l
-> Name l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
Scope l
-> Name l -> ScopedAST NameBinder sig n -> AST NameBinder sig l
openWith Scope l
scope' (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
b) ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret
          -- The binders are named here, in the move, freshened against the
          -- names taken at the hole: an anonymous binder would otherwise be
          -- named at render time (bypassing the freshening), and an
          -- accepted move must not shadow anything visible.
          named :: Binder
named = case Binder
orig of
            BinderVar Maybe VarIdent
mx -> Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just (Set VarIdent -> VarIdent -> VarIdent
refreshVarIn Set VarIdent
taken (VarIdent -> Maybe VarIdent -> VarIdent
forall a. a -> Maybe a -> a
fromMaybe VarIdent
"x₁" Maybe VarIdent
mx)))
            Binder
other        -> Set VarIdent -> Binder -> Binder
freshenBinderLeavesIn Set VarIdent
taken Binder
other
          taken' :: Set VarIdent
taken' = (VarIdent -> Set VarIdent -> Set VarIdent)
-> Set VarIdent -> [VarIdent] -> Set VarIdent
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr VarIdent -> Set VarIdent -> Set VarIdent
forall a. Ord a => a -> Set a -> Set a
Set.insert Set VarIdent
taken (Binder -> [VarIdent]
binderLeaves Binder
named)
       in TermT n
-> Binder
-> Maybe
     (LambdaParam
        (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n
forall (n :: S).
TermT n
-> Binder
-> Maybe (LambdaParam (ScopedTermT n) (TermT n))
-> ScopedTermT n
-> TermT n
lambdaT TermT n
ty Binder
named Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
forall a. Maybe a
Nothing (NameBinder n l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder n l
b (Set VarIdent
-> Scope l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S).
Distinct n =>
Set VarIdent -> Scope n -> TermT n -> TermT n
lambdaHoleOf Set VarIdent
taken' Scope l
scope' AST NameBinder (AnnSig TypeInfo TermSig) l
retAt))
  TermT n
_ -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
ty

-- | A match over a hypothesis, one branch per constructor with a hole body:
-- the notational candidate offered beside the @ind-@\/@rec-@ spines. The node
-- is display-only (its annotations are dropped before rendering), so its type
-- infos are holes. Branch binders reuse the constructor's declared field
-- names, with an induction hypothesis named @ih@, freshened against the names
-- taken at the hole exactly as 'lambdaHoleOf' freshens its motive binders.
matchHoleOf
  :: Distinct n
  => Context n -> Set.Set VarIdent -> Foil.Scope n
  -> Int -> [Foil.Name n] -> TermT n -> TermT n
matchHoleOf :: forall (n :: S).
Distinct n =>
Context n
-> Set VarIdent -> Scope n -> Int -> [Name n] -> TermT n -> TermT n
matchHoleOf Context n
ctx Set VarIdent
taken Scope n
scope Int
numParams [Name n]
cons TermT n
term =
  TypeInfo (TermT n)
-> TermT n -> Maybe (TermT n) -> [(VarIdent, TermT n)] -> TermT n
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> AST binder (AnnSig ann TermSig) n
-> Maybe (AST binder (AnnSig ann TermSig) n)
-> [(VarIdent, AST binder (AnnSig ann TermSig) n)]
-> AST binder (AnnSig ann TermSig) n
MatchT TypeInfo (TermT n)
forall (x :: S). TypeInfo (TermT x)
anyInfo TermT n
term Maybe (TermT n)
forall a. Maybe a
Nothing
    [ (VarIdent
name, Scope n -> [Binder] -> TermT n
forall (x :: S). Distinct x => Scope x -> [Binder] -> TermT x
armChain Scope n
scope (Name n -> [Binder]
branchBinders Name n
c))
    | Name n
c <- [Name n]
cons
    , Just VarIdent
name <- [Binder -> Maybe VarIdent
binderName (VarInfo n -> Binder
forall (n :: S). VarInfo n -> Binder
varOrig (Name n -> Context n -> VarInfo n
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name n
c Context n
ctx))]
    ]
  where
    anyInfo :: TypeInfo (TermT x)
    anyInfo :: forall (x :: S). TypeInfo (TermT x)
anyInfo = TypeInfo { infoType :: TermT x
infoType = TermT x -> TermT x
forall (n :: S). TermT n -> TermT n
mkHole TermT x
forall (n :: S). TermT n
universeT, infoWHNF :: Maybe (TermT x)
infoWHNF = Maybe (TermT x)
forall a. Maybe a
Nothing, infoNF :: Maybe (TermT x)
infoNF = Maybe (TermT x)
forall a. Maybe a
Nothing }

    -- one binder per method argument: the declared fields, each recursive
    -- field followed by its induction hypothesis
    branchBinders :: Name n -> [Binder]
branchBinders Name n
c =
      let info :: VarInfo n
info = Name n -> Context n -> VarInfo n
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name n
c Context n
ctx
          (Int
numFields, [Int]
recIdxs) = case VarInfo n -> Maybe (DataRole n)
forall (n :: S). VarInfo n -> Maybe (DataRole n)
varDataRole VarInfo n
info of
            Just (DataRole Name n
_ Int
_ (DataConKind ConSort
_ Int
_ Int
nf [Int]
ri)) -> (Int
nf, [Int]
ri)
            Maybe (DataRole n)
_                                         -> (Int
0, [])
          fields :: [Binder]
fields = Int -> Int -> TermT n -> [Binder]
forall (x :: S). Int -> Int -> TermT x -> [Binder]
piBinders Int
numParams Int
numFields (VarInfo n -> TermT n
forall (n :: S). VarInfo n -> TermT n
varType VarInfo n
info)
       in Set VarIdent -> [Binder] -> [Binder]
named Set VarIdent
taken ([[Binder]] -> [Binder]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ Binder
b Binder -> [Binder] -> [Binder]
forall a. a -> [a] -> [a]
: [ Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
"ih") | Int
j Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
recIdxs ]
            | (Int
j, Binder
b) <- [Int] -> [Binder] -> [(Int, Binder)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
0 :: Int) ..] [Binder]
fields ])

    -- the binders of a Π-chain: skip the parameters, take the fields
    piBinders :: Int -> Int -> TermT x -> [Binder]
    piBinders :: forall (x :: S). Int -> Int -> TermT x -> [Binder]
piBinders Int
_ Int
0 TermT x
_ = []
    piBinders Int
skip Int
take_ (TypeFunT TypeInfo (TermT x)
_ Binder
orig TModality
_ TermT x
_ Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) x)
_ (ScopedAST NameBinder x l
_ AST NameBinder (AnnSig TypeInfo TermSig) l
body))
      | Int
skip Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0  = Int
-> Int -> AST NameBinder (AnnSig TypeInfo TermSig) l -> [Binder]
forall (x :: S). Int -> Int -> TermT x -> [Binder]
piBinders (Int
skip Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
take_ AST NameBinder (AnnSig TypeInfo TermSig) l
body
      | Bool
otherwise = Binder
orig Binder -> [Binder] -> [Binder]
forall a. a -> [a] -> [a]
: Int
-> Int -> AST NameBinder (AnnSig TypeInfo TermSig) l -> [Binder]
forall (x :: S). Int -> Int -> TermT x -> [Binder]
piBinders Int
0 (Int
take_ Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) AST NameBinder (AnnSig TypeInfo TermSig) l
body
    piBinders Int
_ Int
_ TermT x
_ = []

    named :: Set VarIdent -> [Binder] -> [Binder]
named Set VarIdent
_ [] = []
    named Set VarIdent
taken' (Binder
b : [Binder]
bs) =
      let b' :: Binder
b' = case Binder
b of
            BinderVar Maybe VarIdent
mx -> Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just (Set VarIdent -> VarIdent -> VarIdent
refreshVarIn Set VarIdent
taken' (VarIdent -> Maybe VarIdent -> VarIdent
forall a. a -> Maybe a -> a
fromMaybe VarIdent
"x₁" Maybe VarIdent
mx)))
            Binder
other        -> Set VarIdent -> Binder -> Binder
freshenBinderLeavesIn Set VarIdent
taken' Binder
other
          taken'' :: Set VarIdent
taken'' = (VarIdent -> Set VarIdent -> Set VarIdent)
-> Set VarIdent -> [VarIdent] -> Set VarIdent
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr VarIdent -> Set VarIdent -> Set VarIdent
forall a. Ord a => a -> Set a -> Set a
Set.insert Set VarIdent
taken' (Binder -> [VarIdent]
binderLeaves Binder
b')
       in Binder
b' Binder -> [Binder] -> [Binder]
forall a. a -> [a] -> [a]
: Set VarIdent -> [Binder] -> [Binder]
named Set VarIdent
taken'' [Binder]
bs

    armChain :: Distinct x => Foil.Scope x -> [Binder] -> TermT x
    armChain :: forall (x :: S). Distinct x => Scope x -> [Binder] -> TermT x
armChain Scope x
_ [] = TermT x -> TermT x
forall (n :: S). TermT n -> TermT n
mkHole (TermT x -> TermT x
forall (n :: S). TermT n -> TermT n
mkHole TermT x
forall (n :: S). TermT n
universeT)
    armChain Scope x
sc (Binder
b : [Binder]
bs) = Scope x
-> (forall (l :: S). DExt x l => NameBinder x l -> TermT x)
-> TermT x
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope x
sc ((forall (l :: S). DExt x l => NameBinder x l -> TermT x)
 -> TermT x)
-> (forall (l :: S). DExt x l => NameBinder x l -> TermT x)
-> TermT x
forall a b. (a -> b) -> a -> b
$ \NameBinder x l
nb ->
      TypeInfo (TermT x)
-> Binder
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) x
-> TermT x
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
ann (AST binder (AnnSig ann TermSig) n)
-> Binder
-> ScopedAST binder (AnnSig ann TermSig) n
-> AST binder (AnnSig ann TermSig) n
MatchArmT TypeInfo (TermT x)
forall (x :: S). TypeInfo (TermT x)
anyInfo Binder
b (NameBinder x l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) x
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder x l
nb (Scope l -> [Binder] -> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (x :: S). Distinct x => Scope x -> [Binder] -> TermT x
armChain (NameBinder x l -> Scope x -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder x l
nb Scope x
sc) [Binder]
bs))

-- | Apply a term along its Π-type: a 'Just' is the argument to use, a
-- 'Nothing' becomes a typed hole. Stops when the plan runs out.
applyPlan :: Distinct n => TermT n -> [Maybe (TermT n)] -> TypeCheck n (TermT n)
applyPlan :: forall (n :: S).
Distinct n =>
TermT n -> [Maybe (TermT n)] -> TypeCheck n (TermT n)
applyPlan TermT n
t [] = TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
t
applyPlan TermT n
t (Maybe (TermT n)
planned : [Maybe (TermT n)]
plan) = TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
t ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (TermT n)
-> (TermT n
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (TermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  TypeFunT TypeInfo (TermT n)
_info Binder
_orig TModality
_md TermT n
param Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret -> do
    let arg :: TermT n
arg = case Maybe (TermT n)
planned of
          Just TermT n
a  -> TermT n
a
          Maybe (TermT n)
Nothing -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
param
    retAt <- ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall (n :: S).
Distinct n =>
ScopedTermT n -> TermT n -> TypeCheck n (TermT n)
instantiate ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret TermT n
arg
    applyPlan (appT retAt t arg) plan
  TermT n
_ -> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
t

-- | How many /branching/ eliminators 'allEliminationsInto' will chain.
--
-- A forced Π-application is free (see 'allEliminationsInto'), so this bounds only
-- the Σ/cube projections and @idJ@ steps, not the argument count of a spine. A
-- temporary fixed bound: branching is shallow in the goals seen so far (a few
-- projections), and a larger bound mostly adds self-referential spines (a built
-- result eliminated again).
maxEliminationDepth :: Int
maxEliminationDepth :: Int
maxEliminationDepth = Int
7

-- | Whether eliminating a value spends the search budget. A forced Π-application
-- is a 'SpineStep' — there is one way to fill the argument (with a hole), so
-- 'allEliminationsInto' applies it for free; a 'Branching' eliminator (a Σ/cube
-- projection or @idJ@) costs one against 'maxEliminationDepth'.
data ElimCost = SpineStep | Branching
  deriving (ElimCost -> ElimCost -> Bool
(ElimCost -> ElimCost -> Bool)
-> (ElimCost -> ElimCost -> Bool) -> Eq ElimCost
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ElimCost -> ElimCost -> Bool
== :: ElimCost -> ElimCost -> Bool
$c/= :: ElimCost -> ElimCost -> Bool
/= :: ElimCost -> ElimCost -> Bool
Eq, Int -> ElimCost -> String -> String
[ElimCost] -> String -> String
ElimCost -> String
(Int -> ElimCost -> String -> String)
-> (ElimCost -> String)
-> ([ElimCost] -> String -> String)
-> Show ElimCost
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> ElimCost -> String -> String
showsPrec :: Int -> ElimCost -> String -> String
$cshow :: ElimCost -> String
show :: ElimCost -> String
$cshowList :: [ElimCost] -> String -> String
showList :: [ElimCost] -> String -> String
Show)

-- | All ways to eliminate a hypothesis into a value usable at a goal.
--
-- Given a @target@ type and a hypothesis /term/, return every elimination spine
-- over that term whose type fits the target (or a subtype of it). Arguments
-- introduced by application are left as holes for the caller to fill later. A
-- value that already fits is returned as-is; a function is applied to holes; a
-- Σ-type (or anything that unfolds to one, e.g. @is-contr@) is projected, possibly
-- repeatedly — so @first (first (is-segal-A ? ? ? ? ?))@ is discovered.
--
-- A Π-application is a forced spine step, so it extends the spine for free and
-- does not spend the budget. Only the genuinely branching eliminators count
-- against 'maxEliminationDepth', so the bound limits real search depth, not
-- argument count, and a lemma that must be applied to many holes is still reached.
--
-- A spine over a top-level hypothesis is emitted only once its meta prefix
-- (see "Rzk.TypeCheck.MetaPrefix") is fully applied: an unsaturated schema
-- is not a suggestion, mirroring the warn-meta-prefix discipline. The search
-- still passes through the unsaturated stages, so the saturated spines
-- behind them are found; only the emission is gated.
allEliminationsInto
  :: Distinct n => TermT n -> Set.Set VarIdent -> TermT n -> TypeCheck n [TermT n]
allEliminationsInto :: forall (n :: S).
Distinct n =>
TermT n -> Set VarIdent -> TermT n -> TypeCheck n [TermT n]
allEliminationsInto TermT n
target Set VarIdent
takenNames TermT n
hyp = do
  minApps <- case TermT n
hyp of
    Var Name n
v -> (Context n -> Int)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (VarInfo n -> Int
forall (n :: S). VarInfo n -> Int
varMetaPrefix (VarInfo n -> Int) -> (Context n -> VarInfo n) -> Context n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name n -> Context n -> VarInfo n
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name n
v)
    TermT n
_     -> Int
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) Int
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0
  go minApps maxEliminationDepth hyp
  where
    go :: Int
-> Int
-> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
go Int
minApps Int
depth TermT n
term = do
      ty    <- TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
term
      fits  <- if minApps <= 0 then fitsInto term ty target else pure False
      elims <- eliminatorsOf takenNames ty
      let step (ElimCost
SpineStep, TermT n -> TypeCheck n (TermT n)
wrap) = Int
-> Int
-> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
go (Int
minApps Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
depth (TermT n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [TermT n])
-> TypeCheck n (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TermT n -> TypeCheck n (TermT n)
wrap TermT n
term
          step (ElimCost
Branching, TermT n -> TypeCheck n (TermT n)
wrap)
            | Int
depth Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [TermT n]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
            | Bool
otherwise  = Int
-> Int
-> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
go Int
minApps (Int
depth Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (TermT n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [TermT n])
-> TypeCheck n (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TermT n -> TypeCheck n (TermT n)
wrap TermT n
term
      deeper <- concat <$> mapM step elims
      pure ([term | fits] <> deeper)

-- | Whether a term of the given (whnf) type may stand where a value of the
-- @target@ type is expected: the two types unify under 'structuralHoleUnify', so a
-- hole acts as a wildcard leaf but a structural mismatch around it is still a
-- mismatch (an under-applied function does not match an extension-type goal, but a
-- partial application that genuinely fits an ordinary-function goal does).
--
-- The exception is a /flexible/ type, one headed by a hole: it has no shape to
-- mismatch with, so it fits any target. This is what makes an eliminator stated
-- over a motive usable as a candidate --- @ind-path ? ? ? ? ? ?@ has type
-- @?C ?x ?p@ and so is offered at every goal, exactly as @idJ@ already is, with
-- the motive and the base case left as holes.
--
-- Outer type restrictions are stripped from both sides first: an extension-type
-- boundary is satisfied by later refinement, not by the choice of spine, and
-- matching against the restricted goal would reject the very spine that introduces
-- the holes meant to satisfy it (@f ?@ at a boundary goal, say).
--
-- Holes or constraints recorded while probing are discarded, so this is a pure
-- yes\/no query.
fitsInto :: Distinct n => TermT n -> TermT n -> TermT n -> TypeCheck n Bool
fitsInto :: forall (n :: S).
Distinct n =>
TermT n -> TermT n -> TermT n -> TypeCheck n Bool
fitsInto TermT n
term TermT n
ty TermT n
target = do
  ty'     <- TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
stripTypeRestrictions (TermT n -> TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TermT n
ty
  target' <- stripTypeRestrictions <$> whnfT target
  suppressing $ local structuralHoleUnify
    ((unify (Just term) target' ty' >> pure True) `catchError` \TypeErrorInScopedContext
_ -> Bool -> TypeCheck n Bool
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False)

-- | The eliminators a value of the given (weak head normal) type admits, each as a
-- function wrapping the eliminated term, paired with its 'ElimCost'.
--
-- A Π-type is eliminated by application to a fresh hole (a spine step); a Σ-type by
-- either projection; an identity type by path induction (@idJ@), with the motive
-- and base case left as holes. The projections and @idJ@ branch. Anything else
-- admits no simple eliminator.
--
-- The names taken at the hole (the source namespace) are passed in so that
-- every binder an eliminator introduces (the @idJ@ motive's @\\ b q → ?@, a
-- data eliminator's motive λs) is named in the move, freshened against them.
eliminatorsOf
  :: Distinct n
  => Set.Set VarIdent -> TermT n -> TypeCheck n [(ElimCost, TermT n -> TypeCheck n (TermT n))]
eliminatorsOf :: forall (n :: S).
Distinct n =>
Set VarIdent
-> TermT n
-> TypeCheck n [(ElimCost, TermT n -> TypeCheck n (TermT n))]
eliminatorsOf Set VarIdent
takenNames TermT n
ty =
  case TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
stripTypeRestrictions TermT n
ty of
    TypeFunT TypeInfo (TermT n)
_ty Binder
orig TModality
_md TermT n
param Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret ->
      [(ElimCost, TermT n -> TypeCheck n (TermT n))]
-> TypeCheck n [(ElimCost, TermT n -> TypeCheck n (TermT n))]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ (ElimCost
SpineStep, \TermT n
term -> do
                let h :: TermT n
h = Maybe VarIdent -> TermT n -> TermT n
forall (n :: S). Maybe VarIdent -> TermT n -> TermT n
mkNamedHole (Binder -> Maybe VarIdent
binderName Binder
orig) TermT n
param
                retAt <- ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
ScopedTermT n -> TermT n -> TypeCheck n (TermT n)
instantiate ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret TermT n
h
                pure (appT retAt term h)) ]
    TypeSigmaT TypeInfo (TermT n)
_ty Binder
_orig TModality
_md TermT n
a ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
b ->
      [(ElimCost, TermT n -> TypeCheck n (TermT n))]
-> TypeCheck n [(ElimCost, TermT n -> TypeCheck n (TermT n))]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ (ElimCost
Branching, \TermT n
term -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT TermT n
a TermT n
term))
           , (ElimCost
Branching, \TermT n
term -> do
                bAt <- ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
ScopedTermT n -> TermT n -> TypeCheck n (TermT n)
instantiate ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
b (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT TermT n
a TermT n
term)
                pure (secondT bAt term)) ]
    -- A cube point pair (a pattern-bound @(t , s) : 2 × 2@, say) projects to its
    -- coordinates; rzk renders those projections back as the pattern names.
    CubeProductT TypeInfo (TermT n)
_ty TermT n
a TermT n
b ->
      [(ElimCost, TermT n -> TypeCheck n (TermT n))]
-> TypeCheck n [(ElimCost, TermT n -> TypeCheck n (TermT n))]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ (ElimCost
Branching, \TermT n
term -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT TermT n
a TermT n
term))
           , (ElimCost
Branching, \TermT n
term -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
secondT TermT n
b TermT n
term)) ]
    -- A path @p : a =_A x@ is eliminated by path induction. The motive
    -- @C : (z : A) → (a =_A z) → U@ is always a function, so we introduce it
    -- straight away as @\\ b q → ?@ rather than leaving it a bare hole: the spine
    -- @idJ A a (\\ b q → ?) ? x p@ then has type @C x p@, which β-reduces to that
    -- inner hole — so J fits any goal (the player fills the motive and the base case
    -- @d : C a refl@). The two holes are the motive predicate and the base.
    TypeIdT TypeInfo (TermT n)
_ty TermT n
a Maybe (TermT n)
mtA TermT n
x -> do
      tA <- TypeCheck n (TermT n)
-> (TermT n -> TypeCheck n (TermT n))
-> Maybe (TermT n)
-> TypeCheck n (TermT n)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
a) TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (TermT n)
mtA
      scope <- asks ctxScope
      let c = Set VarIdent -> Scope n -> TermT n -> TermT n -> TermT n
forall (n :: S).
Distinct n =>
Set VarIdent -> Scope n -> TermT n -> TermT n -> TermT n
motiveOf Set VarIdent
takenNames Scope n
scope TermT n
a TermT n
tA
          dType = TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT TermT n
forall (n :: S). TermT n
universeT
                    (TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT (Binder
-> TModality
-> TermT n
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n
forall (n :: S).
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
typeFunT (Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing) TModality
Id (TermT n -> Maybe (TermT n) -> TermT n -> TermT n
forall (n :: S). TermT n -> Maybe (TermT n) -> TermT n -> TermT n
typeIdT TermT n
a (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
tA) TermT n
a) Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. Maybe a
Nothing
                            (Scope n
-> (forall (n :: S). TermT n)
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S).
Distinct n =>
Scope n -> (forall (n :: S). TermT n) -> ScopedTermT n
closedScope Scope n
scope TermT l
forall (n :: S). TermT n
universeT))
                      TermT n
c TermT n
a)
                    (TermT n -> Maybe (TermT n, Maybe (TermT n)) -> TermT n
forall (n :: S).
TermT n -> Maybe (TermT n, Maybe (TermT n)) -> TermT n
reflT (TermT n -> Maybe (TermT n) -> TermT n -> TermT n
forall (n :: S). TermT n -> Maybe (TermT n) -> TermT n -> TermT n
typeIdT TermT n
a (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
tA) TermT n
a) Maybe (TermT n, Maybe (TermT n))
forall a. Maybe a
Nothing)
          d = TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
dType
          motiveAt TermT n
y TermT n
p = TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT TermT n
forall (n :: S). TermT n
universeT
            (TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT (Binder
-> TModality
-> TermT n
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n
forall (n :: S).
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
typeFunT (Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing) TModality
Id (TermT n -> Maybe (TermT n) -> TermT n -> TermT n
forall (n :: S). TermT n -> Maybe (TermT n) -> TermT n -> TermT n
typeIdT TermT n
a (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
tA) TermT n
y) Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. Maybe a
Nothing
                    (Scope n
-> (forall (n :: S). TermT n)
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S).
Distinct n =>
Scope n -> (forall (n :: S). TermT n) -> ScopedTermT n
closedScope Scope n
scope TermT l
forall (n :: S). TermT n
universeT))
              TermT n
c TermT n
y) TermT n
p
      pure [ (Branching, \TermT n
p -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
forall (n :: S).
TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
-> TermT n
idJT (TermT n -> TermT n -> TermT n
motiveAt TermT n
x TermT n
p) TermT n
tA TermT n
a TermT n
c TermT n
d TermT n
x TermT n
p)) ]
    -- A value of a #data type is eliminated by its generated eliminators:
    -- the parameters and indices are read off the hypothesis's type, the
    -- motive and methods are left as holes. The match notation for the same
    -- elimination is offered first, one hole per branch (an empty family has
    -- no branch syntax, so it gets only the eliminators).
    TermT n
other -> case TermT n -> (TermT n, [(TypeInfo (TermT n), TermT n)])
forall (n :: S).
TermT n -> (TermT n, [(TypeInfo (TermT n), TermT n)])
collectAppSpine TermT n
other of
      (Var Name n
d, [(TypeInfo (TermT n), TermT n)]
dargs0) -> do
        let dargs :: [TermT n]
dargs = ((TypeInfo (TermT n), TermT n) -> TermT n)
-> [(TypeInfo (TermT n), TermT n)] -> [TermT n]
forall a b. (a -> b) -> [a] -> [b]
map (TypeInfo (TermT n), TermT n) -> TermT n
forall a b. (a, b) -> b
snd [(TypeInfo (TermT n), TermT n)]
dargs0
        elims <- Name n -> TypeCheck n [(Name n, DataRole n)]
forall (n :: S). Name n -> TypeCheck n [(Name n, DataRole n)]
dataEliminatorsOf Name n
d
        cons <- dataConstructorsOf d
        ctx <- ask
        scope <- asks ctxScope
        let matchMoves =
              [ (ElimCost
Branching, \TermT n
term ->
                  TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context n
-> Set VarIdent -> Scope n -> Int -> [Name n] -> TermT n -> TermT n
forall (n :: S).
Distinct n =>
Context n
-> Set VarIdent -> Scope n -> Int -> [Name n] -> TermT n -> TermT n
matchHoleOf Context n
ctx Set VarIdent
takenNames Scope n
scope Int
numParams [Name n]
cons TermT n
term))
              | Bool -> Bool
not ([Name n] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name n]
cons)
              , (Name n
_, DataRole Name n
_ Int
numParams DataRoleKind
_) : [(Name n, DataRole n)]
_ <- [[(Name n, DataRole n)]
elims]
              ]
            elimSpines =
              [ (ElimCost
Branching, \TermT n
term -> do
                  let ([TermT n]
paramArgs, [TermT n]
indexArgs) = Int -> [TermT n] -> ([TermT n], [TermT n])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
numParams [TermT n]
dargs
                  atMotive <- TermT n -> [Maybe (TermT n)] -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
TermT n -> [Maybe (TermT n)] -> TypeCheck n (TermT n)
applyPlan (Name n -> TermT n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
e) ((TermT n -> Maybe (TermT n)) -> [TermT n] -> [Maybe (TermT n)]
forall a b. (a -> b) -> [a] -> [b]
map TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just [TermT n]
paramArgs)
                  -- The motive is a λ over a hole (not a bare hole), so the
                  -- eliminator's result type β-reduces to the hole and fits
                  -- any goal; cf. the idJ case above.
                  motive <- typeOf atMotive >>= \case
                    TypeFunT TypeInfo (TermT n)
_ Binder
_ TModality
_ TermT n
motiveTy Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_ ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
_ -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set VarIdent -> Scope n -> TermT n -> TermT n
forall (n :: S).
Distinct n =>
Set VarIdent -> Scope n -> TermT n -> TermT n
lambdaHoleOf Set VarIdent
takenNames Scope n
scope TermT n
motiveTy)
                    TermT n
_ -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
forall (n :: S). TermT n
universeT)
                  applyPlan atMotive
                    (Just motive : replicate numMethods Nothing
                      <> map Just indexArgs <> [Just term]))
              | (Name n
e, DataRole Name n
_ Int
numParams (DataElimKind Int
numMethods Int
_numIndices ElimKind
_)) <- [(Name n, DataRole n)]
elims ]
        pure (matchMoves <> elimSpines)
      (TermT n, [(TypeInfo (TermT n), TermT n)])
_ -> [(ElimCost, TermT n -> TypeCheck n (TermT n))]
-> TypeCheck n [(ElimCost, TermT n -> TypeCheck n (TermT n))]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

-- | A scoped term that does not use its binder.
closedScope :: Distinct n => Foil.Scope n -> (forall l. TermT l) -> ScopedTermT n
closedScope :: forall (n :: S).
Distinct n =>
Scope n -> (forall (n :: S). TermT n) -> ScopedTermT n
closedScope Scope n
scope forall (n :: S). TermT n
t = Scope n
-> (forall (l :: S). DExt n l => NameBinder n l -> ScopedTermT n)
-> ScopedTermT n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall (l :: S). DExt n l => NameBinder n l -> ScopedTermT n)
 -> ScopedTermT n)
-> (forall (l :: S). DExt n l => NameBinder n l -> ScopedTermT n)
-> ScopedTermT n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder -> NameBinder n l
-> AST NameBinder (AnnSig TypeInfo TermSig) l -> ScopedTermT n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder n l
binder AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S). TermT n
t

-- | The motive @\\ b q → ?@ of a path induction: a type in the two motive binders,
-- left as a hole.
motiveOf :: Distinct n => Set.Set VarIdent -> Foil.Scope n -> TermT n -> TermT n -> TermT n
motiveOf :: forall (n :: S).
Distinct n =>
Set VarIdent -> Scope n -> TermT n -> TermT n -> TermT n
motiveOf Set VarIdent
takenNames Scope n
scope TermT n
a TermT n
tA =
  Scope n
-> (forall (l :: S). DExt n l => NameBinder n l -> TermT n)
-> TermT n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall (l :: S). DExt n l => NameBinder n l -> TermT n)
 -> TermT n)
-> (forall (l :: S). DExt n l => NameBinder n l -> TermT n)
-> TermT n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
bBinder ->
    let scopeB :: Scope l
scopeB = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
bBinder Scope n
scope
        b :: AST NameBinder (AnnSig TypeInfo TermSig) l
b = Name l -> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
bBinder)
        idTypeAtB :: AST NameBinder (AnnSig TypeInfo TermSig) l
idTypeAtB = AST NameBinder (AnnSig TypeInfo TermSig) l
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) l)
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S). TermT n -> Maybe (TermT n) -> TermT n -> TermT n
typeIdT (TermT n -> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
a) (AST NameBinder (AnnSig TypeInfo TermSig) l
-> Maybe (AST NameBinder (AnnSig TypeInfo TermSig) l)
forall a. a -> Maybe a
Just (TermT n -> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
tA)) AST NameBinder (AnnSig TypeInfo TermSig) l
b
        -- the motive's own binders must not shadow anything visible at the
        -- hole (the move is inserted as source text)
        bName :: VarIdent
bName = Set VarIdent -> VarIdent -> VarIdent
refreshVarIn Set VarIdent
takenNames VarIdent
"b"
        qName :: VarIdent
qName = Set VarIdent -> VarIdent -> VarIdent
refreshVarIn (VarIdent -> Set VarIdent -> Set VarIdent
forall a. Ord a => a -> Set a -> Set a
Set.insert VarIdent
bName Set VarIdent
takenNames) VarIdent
"q"
     in Scope l
-> (forall (l :: S). DExt l l => NameBinder l l -> TermT n)
-> TermT n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope l
scopeB ((forall (l :: S). DExt l l => NameBinder l l -> TermT n)
 -> TermT n)
-> (forall (l :: S). DExt l l => NameBinder l l -> TermT n)
-> TermT n
forall a b. (a -> b) -> a -> b
$ \NameBinder l l
qBinder ->
          let cBody :: TermT n
cBody = TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
forall (n :: S). TermT n
universeT
              cInner :: AST NameBinder (AnnSig TypeInfo TermSig) l
cInner = AST NameBinder (AnnSig TypeInfo TermSig) l
-> Binder
-> Maybe
     (LambdaParam
        (ScopedTermT l) (AST NameBinder (AnnSig TypeInfo TermSig) l))
-> ScopedTermT l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S).
TermT n
-> Binder
-> Maybe (LambdaParam (ScopedTermT n) (TermT n))
-> ScopedTermT n
-> TermT n
lambdaT
                (Binder
-> TModality
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> Maybe (ScopedTermT l)
-> ScopedTermT l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S).
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
typeFunT (Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing) TModality
Id AST NameBinder (AnnSig TypeInfo TermSig) l
idTypeAtB Maybe (ScopedTermT l)
forall a. Maybe a
Nothing
                  (NameBinder l l
-> AST NameBinder (AnnSig TypeInfo TermSig) l -> ScopedTermT l
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder l l
qBinder AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S). TermT n
universeT))
                (Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
qName)) Maybe
  (LambdaParam
     (ScopedTermT l) (AST NameBinder (AnnSig TypeInfo TermSig) l))
forall a. Maybe a
Nothing
                (NameBinder l l
-> AST NameBinder (AnnSig TypeInfo TermSig) l -> ScopedTermT l
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder l l
qBinder AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S). TermT n
cBody)
              cType :: TermT n
cType = Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
forall (n :: S).
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
typeFunT (Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing) TModality
Id TermT n
tA Maybe (ScopedTermT n)
forall a. Maybe a
Nothing
                (NameBinder n l
-> AST NameBinder (AnnSig TypeInfo TermSig) l -> ScopedTermT n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder n l
bBinder
                  (Binder
-> TModality
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> Maybe (ScopedTermT l)
-> ScopedTermT l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S).
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
typeFunT (Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing) TModality
Id AST NameBinder (AnnSig TypeInfo TermSig) l
idTypeAtB Maybe (ScopedTermT l)
forall a. Maybe a
Nothing
                    (NameBinder l l
-> AST NameBinder (AnnSig TypeInfo TermSig) l -> ScopedTermT l
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder l l
qBinder AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S). TermT n
universeT)))
           in TermT n
-> Binder
-> Maybe (LambdaParam (ScopedTermT n) (TermT n))
-> ScopedTermT n
-> TermT n
forall (n :: S).
TermT n
-> Binder
-> Maybe (LambdaParam (ScopedTermT n) (TermT n))
-> ScopedTermT n
-> TermT n
lambdaT TermT n
cType (Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
bName)) Maybe (LambdaParam (ScopedTermT n) (TermT n))
forall a. Maybe a
Nothing (NameBinder n l
-> AST NameBinder (AnnSig TypeInfo TermSig) l -> ScopedTermT n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder n l
bBinder AST NameBinder (AnnSig TypeInfo TermSig) l
cInner)

-- | The binder for a λ introduced over a domain type.
--
-- A binder the type already gives as a pattern is kept as-is — it carries the
-- user's own names (@(t , s)@). Otherwise an /explicit/ (pre-whnf) Σ-type or
-- product domain is destructured into a fresh pair pattern, recursively for
-- products, so that a nameless @2 × 2 × 2@ parameter is introduced as
-- @((t1 , t2) , t3)@ rather than a single opaque variable. Any other domain keeps
-- its single binder.
--
-- Leaves are named by what they range over: a cube-product component is a point,
-- named @tN@; a Σ component is a term, named @xN@. The names are display-only (the
-- body is a hole that does not mention them) and carry a shared running index, so
-- every leaf in the pattern is distinct.
destructuringBinder :: Binder -> TermT n -> Binder
destructuringBinder :: forall (n :: S). Binder -> TermT n -> Binder
destructuringBinder Binder
orig TermT n
param = case Binder
orig of
  BinderPair{} -> Binder
orig                 -- already a pattern: keep the user's names
  Binder
_ -> case TermT n
param of
    CubeProductT{} -> (Binder, Int) -> Binder
forall a b. (a, b) -> a
fst (Int -> TermT n -> (Binder, Int)
forall {a} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
(Show a, Num a) =>
a -> AST binder (AnnSig ann TermSig) n -> (Binder, a)
go (Int
1 :: Int) TermT n
param)
    TypeSigmaT{}   -> (Binder, Int) -> Binder
forall a b. (a, b) -> a
fst (Int -> TermT n -> (Binder, Int)
forall {a} {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
(Show a, Num a) =>
a -> AST binder (AnnSig ann TermSig) n -> (Binder, a)
go (Int
1 :: Int) TermT n
param)
    TermT n
_              -> Binder
orig             -- not a product/Σ: leave the binder alone
  where
    -- a product/Σ becomes a pair; we recurse into a product's components (plain
    -- types) but not under a Σ's binder (a scope). A leaf is named by its enclosing
    -- constructor: @tN@ under a cube product, @xN@ under a Σ.
    go :: a -> AST binder (AnnSig ann TermSig) n -> (Binder, a)
go a
n = \case
      CubeProductT ann (AST binder (AnnSig ann TermSig) n)
_ AST binder (AnnSig ann TermSig) n
a AST binder (AnnSig ann TermSig) n
b ->
        let (Binder
l, a
n')  = String -> a -> AST binder (AnnSig ann TermSig) n -> (Binder, a)
child String
"t" a
n  AST binder (AnnSig ann TermSig) n
a
            (Binder
r, a
n'') = String -> a -> AST binder (AnnSig ann TermSig) n -> (Binder, a)
child String
"t" a
n' AST binder (AnnSig ann TermSig) n
b
        in (Binder -> Binder -> Binder
BinderPair Binder
l Binder
r, a
n'')
      TypeSigmaT ann (AST binder (AnnSig ann TermSig) n)
_ Binder
_ TModality
_md AST binder (AnnSig ann TermSig) n
a ScopedAST binder (AnnSig ann TermSig) n
_b ->
        let (Binder
l, a
n') = String -> a -> AST binder (AnnSig ann TermSig) n -> (Binder, a)
child String
"x" a
n AST binder (AnnSig ann TermSig) n
a
        in (Binder -> Binder -> Binder
BinderPair Binder
l (Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just (String -> a -> VarIdent
forall {a} {a}. (IsString a, Show a) => String -> a -> a
leaf String
"x" a
n'))), a
n' a -> a -> a
forall a. Num a => a -> a -> a
+ a
1)
      AST binder (AnnSig ann TermSig) n
_ -> (Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just (String -> a -> VarIdent
forall {a} {a}. (IsString a, Show a) => String -> a -> a
leaf String
"t" a
n)), a
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
1)  -- unreached: go is called on products only
    child :: String -> a -> AST binder (AnnSig ann TermSig) n -> (Binder, a)
child String
pfx a
n = \case
      c :: AST binder (AnnSig ann TermSig) n
c@CubeProductT{} -> a -> AST binder (AnnSig ann TermSig) n -> (Binder, a)
go a
n AST binder (AnnSig ann TermSig) n
c
      c :: AST binder (AnnSig ann TermSig) n
c@TypeSigmaT{}   -> a -> AST binder (AnnSig ann TermSig) n -> (Binder, a)
go a
n AST binder (AnnSig ann TermSig) n
c
      AST binder (AnnSig ann TermSig) n
_                -> (Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just (String -> a -> VarIdent
forall {a} {a}. (IsString a, Show a) => String -> a -> a
leaf String
pfx a
n)), a
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
1)
    leaf :: String -> a -> a
leaf String
pfx a
n = String -> a
forall a. IsString a => String -> a
fromString (String
pfx String -> String -> String
forall a. Semigroup a => a -> a -> a
<> a -> String
forall a. Show a => a -> String
show a
n :: String)

-- | All ways to introduce a value /of/ a goal type by its head constructor,
-- leaving the constituents as holes:
--
--   * a Π-type is introduced by a λ-abstraction over a hole body (@\\ x -> ?@); the
--     binder is taken from the type, so a pattern domain (a @Δ²@ point @(t , s)@,
--     say) is introduced as @\\ (t , s) -> ?@;
--   * a Σ-type or a cube product by a pair of holes (@(? , ?)@);
--   * an identity type by @refl@, but only when its two endpoints already agree
--     (otherwise @refl@ would not typecheck);
--   * the unit type by @unit@;
--   * the tope universe by each tope constructor — @TOP@, @BOT@, @? ≡ ?@, @? ≤ ?@,
--     @? ∧ ?@, @? ∨ ?@ — so a shape (a hole of type @TOPE@) can be built up by
--     tapping.
--
-- Unlike 'allEliminationsInto' this does not search: a type has at most one
-- introduction form (the tope universe is the one exception), read off its head
-- constructor. Outer restrictions are stripped first, so an extension type is
-- introduced by the form of its underlying type (its boundary is met by later
-- refinement of the holes, not by the choice of constructor).
--
-- The λ binder of a Π-introduction is freshened against the names already visible
-- at the hole, so introducing over a type whose own definition reuses an in-scope
-- name (@hom@, whose internal binder is @t@) yields @\\ t₁ -> ?@ rather than a @t@
-- that shadows the existing one.
allIntroductionsOf
  :: Distinct n => TermT n -> Set.Set VarIdent -> TypeCheck n [TermT n]
allIntroductionsOf :: forall (n :: S).
Distinct n =>
TermT n -> Set VarIdent -> TypeCheck n [TermT n]
allIntroductionsOf TermT n
target Set VarIdent
takenNames = do
  target' <- TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
stripTypeRestrictions (TermT n -> TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TermT n
target
  scope <- asks ctxScope
  case target' of
    TypeFunT TypeInfo (TermT n)
_ty Binder
orig TModality
_md TermT n
param Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret -> do
      -- An anonymous Π binder (a domain written @B → …@) must still be
      -- named in the offered move: the rendered λ shows its binder, and
      -- leaving the naming to the renderer would bypass the freshening
      -- below, shadowing an enclosing binder that already took the first
      -- default name. Name it here — the first default name, which the
      -- freshening bumps past everything visible at the hole.
      let named :: Binder
named = case Binder -> TermT n -> Binder
forall (n :: S). Binder -> TermT n -> Binder
destructuringBinder Binder
orig TermT n
param of
            BinderVar Maybe VarIdent
Nothing -> Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
"x₁")
            Binder
b                 -> Binder
b
          binder :: Binder
binder = Set VarIdent -> Binder -> Binder
freshenBinderLeavesIn Set VarIdent
takenNames Binder
named
      [TermT n]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TermT n]
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [TermT n])
-> [TermT n]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
forall a b. (a -> b) -> a -> b
$ Scope n
-> (forall (l :: S). DExt n l => NameBinder n l -> [TermT n])
-> [TermT n]
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall (l :: S). DExt n l => NameBinder n l -> [TermT n])
 -> [TermT n])
-> (forall (l :: S). DExt n l => NameBinder n l -> [TermT n])
-> [TermT n]
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
b ->
        let retAt :: AST NameBinder (AnnSig TypeInfo TermSig) l
retAt = Scope l
-> Name l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
Scope l
-> Name l -> ScopedAST NameBinder sig n -> AST NameBinder sig l
openWith (NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
b Scope n
scope) (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
b) ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret
         in [ TermT n
-> Binder
-> Maybe
     (LambdaParam
        (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n
forall (n :: S).
TermT n
-> Binder
-> Maybe (LambdaParam (ScopedTermT n) (TermT n))
-> ScopedTermT n
-> TermT n
lambdaT TermT n
target' Binder
binder Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
forall a. Maybe a
Nothing (NameBinder n l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder n l
b (AST NameBinder (AnnSig TypeInfo TermSig) l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S). TermT n -> TermT n
mkHole AST NameBinder (AnnSig TypeInfo TermSig) l
retAt)) ]
    TypeSigmaT TypeInfo (TermT n)
_ty Binder
_orig TModality
_md TermT n
a ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
b -> do
      let h :: TermT n
h = TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
a
      bAt <- ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall (n :: S).
Distinct n =>
ScopedTermT n -> TermT n -> TypeCheck n (TermT n)
instantiate ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
b TermT n
h
      pure [ pairT target' h (mkHole bAt) ]
    CubeProductT TypeInfo (TermT n)
_ty TermT n
a TermT n
b ->
      [TermT n]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
pairT TermT n
target' (TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
a) (TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
b) ]
    -- the directed interval: its two endpoints are the only closed points, and
    -- they are what a hole in a cube position (@α ? ?@) almost always wants.
    -- The unit cube is offered the same way, for its single point.
    Cube2T{} -> [TermT n]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ TermT n
forall (n :: S). TermT n
cube2_0T, TermT n
forall (n :: S). TermT n
cube2_1T ]
    CubeUnitT{} -> [TermT n]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ TermT n
forall (n :: S). TermT n
cubeUnitStarT ]
    TypeIdT TypeInfo (TermT n)
_ty TermT n
a Maybe (TermT n)
_tA TermT n
b -> do
      agree <- TermT n -> TermT n -> TypeCheck n Bool
forall (n :: S).
Distinct n =>
TermT n -> TermT n -> TypeCheck n Bool
endpointsAgree TermT n
a TermT n
b
      pure [ reflT target' Nothing | agree ]
    TypeUnitT{} -> [TermT n]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ TermT n
forall (n :: S). TermT n
unitT ]
    -- the tope universe: every tope constructor builds a tope, so all are
    -- introductions of a shape goal. Point arguments (of ≡, ≤) and tope arguments
    -- (of ∧, ∨) are left as holes.
    UniverseTopeT{} ->
      let point :: TermT n
point = TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole (TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
forall (n :: S). TermT n
cubeT)  -- a point of an as-yet-unknown cube
          tope :: TermT n
tope  = TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
target'         -- a tope (its type is the tope universe)
       in [TermT n]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ TermT n
forall (n :: S). TermT n
topeTopT, TermT n
forall (n :: S). TermT n
topeBottomT
               , TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT  TermT n
forall (n :: S). TermT n
point TermT n
forall (n :: S). TermT n
point, TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
forall (n :: S). TermT n
point TermT n
forall (n :: S). TermT n
point
               , TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeAndT TermT n
tope  TermT n
tope,  TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeOrT  TermT n
tope  TermT n
tope ]
    -- the universe: a type is built by a type former, so each is an
    -- introduction of a U-goal — a function type, a Σ-type, an identity type,
    -- the unit type, and every user-declared datatype in scope (applied to
    -- holes through its parameter telescope). The Σ binder is named, so it is
    -- freshened like a λ-introduction's binder; the identity type's endpoints
    -- are terms of an as-yet-unknown type, like the tope universe's points.
    UniverseT{} -> do
      ctx <- ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Context n)
forall r (m :: * -> *). MonadReader r m => m r
ask
      let arrow = Binder
-> TModality
-> TermT n
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n
forall (n :: S).
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
typeFunT (Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing) TModality
Id (TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
forall (n :: S). TermT n
universeT) Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. Maybe a
Nothing
                    (Scope n
-> (forall (n :: S). TermT n)
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S).
Distinct n =>
Scope n -> (forall (n :: S). TermT n) -> ScopedTermT n
closedScope Scope n
scope (TermT l -> TermT l
forall (n :: S). TermT n -> TermT n
mkHole TermT l
forall (n :: S). TermT n
universeT))
          sigma = Binder
-> TModality
-> TermT n
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n
forall (n :: S).
Binder -> TModality -> TermT n -> ScopedTermT n -> TermT n
typeSigmaT (Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just (Set VarIdent -> VarIdent -> VarIdent
refreshVarIn Set VarIdent
takenNames VarIdent
"x"))) TModality
Id
                    (TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
forall (n :: S). TermT n
universeT) (Scope n
-> (forall (n :: S). TermT n)
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S).
Distinct n =>
Scope n -> (forall (n :: S). TermT n) -> ScopedTermT n
closedScope Scope n
scope (TermT l -> TermT l
forall (n :: S). TermT n -> TermT n
mkHole TermT l
forall (n :: S). TermT n
universeT))
          endpointTy = TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
forall (n :: S). TermT n
universeT
          identity = TermT n -> Maybe (TermT n) -> TermT n -> TermT n
forall (n :: S). TermT n -> Maybe (TermT n) -> TermT n -> TermT n
typeIdT (TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
forall (n :: S). TermT n
endpointTy) (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
forall (n :: S). TermT n
endpointTy) (TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
forall (n :: S). TermT n
endpointTy)
          formerIds =
            [ Name n -> Int
forall (l :: S). Name l -> Int
Foil.nameId (DataRole n -> Name n
forall (n :: S). DataRole n -> Name n
dataRoleDataType DataRole n
role)
            | (Name n
_, VarInfo n
info) <- Context n -> [(Name n, VarInfo n)]
forall (n :: S). Context n -> [(Name n, VarInfo n)]
varsInScope Context n
ctx
            , Just DataRole n
role <- [VarInfo n -> Maybe (DataRole n)
forall (n :: S). VarInfo n -> Maybe (DataRole n)
varDataRole VarInfo n
info]
            ]
          formers =
            [ Name n
v
            | (Name n
v, VarInfo n
info) <- Context n -> [(Name n, VarInfo n)]
forall (n :: S). Context n -> [(Name n, VarInfo n)]
varsInScope Context n
ctx
            , VarInfo n -> Bool
forall (n :: S). VarInfo n -> Bool
varIsTopLevel VarInfo n
info
            , Name n -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name n
v Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
formerIds
            ]
      datatypes <- mapM (saturateWithHoles . Var) formers
      pure ([arrow, sigma, identity, typeUnitT] <> datatypes)
    -- A goal headed by a #data type former is introduced by a constructor
    -- applied to holes; a constructor whose return indices cannot meet the
    -- goal's (nil against vec A (suc n), say) is filtered out.
    TermT n
_ -> case TermT n -> (TermT n, [(TypeInfo (TermT n), TermT n)])
forall (n :: S).
TermT n -> (TermT n, [(TypeInfo (TermT n), TermT n)])
collectAppSpine TermT n
target' of
      (Var Name n
d, [(TypeInfo (TermT n), TermT n)]
_) -> do
        ctx <- ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Context n)
forall r (m :: * -> *). MonadReader r m => m r
ask
        cons <- dataConstructorsOf d
        fmap concat $ forM cons $ \Name n
c ->
          case VarInfo n -> Maybe (DataRole n)
forall (n :: S). VarInfo n -> Maybe (DataRole n)
varDataRole (Name n -> Context n -> VarInfo n
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name n
c Context n
ctx) of
            Just (DataRole Name n
_ Int
numParams (DataConKind ConSort
_ Int
_ Int
numFields [Int]
_)) -> do
              saturated <- TermT n
-> [Maybe (TermT n)]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall (n :: S).
Distinct n =>
TermT n -> [Maybe (TermT n)] -> TypeCheck n (TermT n)
applyPlan (Name n -> TermT n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
c)
                (Int -> Maybe (TermT n) -> [Maybe (TermT n)]
forall a. Int -> a -> [a]
replicate (Int
numParams Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
numFields) Maybe (TermT n)
forall a. Maybe a
Nothing)
              satTy <- typeOf saturated
              ok <- fitsInto saturated satTy target'
              pure [ saturated | ok ]
            Maybe (DataRole n)
_ -> [TermT n]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
      (TermT n, [(TypeInfo (TermT n), TermT n)])
_ -> [TermT n]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

-- | Apply a term to holes through its whole Π-telescope: a datatype former
-- applied through its parameters, so a @U@-goal offers @coprod ? ?@.
saturateWithHoles :: Distinct n => TermT n -> TypeCheck n (TermT n)
saturateWithHoles :: forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
saturateWithHoles TermT n
term = do
  ty <- TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
term
  case stripTypeRestrictions ty of
    TypeFunT TypeInfo (TermT n)
_ Binder
_ TModality
_ TermT n
param Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_ ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret -> do
      let h :: TermT n
h = TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
param
      retAt <- ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
ScopedTermT n -> TermT n -> TypeCheck n (TermT n)
instantiate ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret TermT n
h
      saturateWithHoles (appT retAt term h)
    TermT n
_ -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
term

-- | Whether the two endpoints of an identity type are definitionally equal, so that
-- @refl@ inhabits it. Like 'fitsInto', any holes or constraints recorded while
-- probing are discarded, leaving a pure yes\/no query.
endpointsAgree :: Distinct n => TermT n -> TermT n -> TypeCheck n Bool
endpointsAgree :: forall (n :: S).
Distinct n =>
TermT n -> TermT n -> TypeCheck n Bool
endpointsAgree TermT n
a TermT n
b =
  TypeCheck n Bool -> TypeCheck n Bool
forall (n :: S) a. TypeCheck n a -> TypeCheck n a
suppressing
    ((Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
forall (n :: S).
Distinct n =>
Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
unify Maybe (TermT n)
forall a. Maybe a
Nothing TermT n
a TermT n
b TypeCheck n () -> TypeCheck n Bool -> TypeCheck n Bool
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> TypeCheck n Bool
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) TypeCheck n Bool
-> (TypeErrorInScopedContext -> TypeCheck n Bool)
-> TypeCheck n Bool
forall a.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TypeErrorInScopedContext
_ -> Bool -> TypeCheck n Bool
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False)

-- | Ex falso: in a contradictory tope context @recBOT@ inhabits any type, so it is a
-- candidate for every goal there (and only there — elsewhere it would not
-- typecheck). Independent of the goal and of the local hypotheses.
recBottomCandidates :: Distinct n => TypeCheck n [TermT n]
recBottomCandidates :: forall (n :: S). Distinct n => TypeCheck n [TermT n]
recBottomCandidates = do
  vacuous <- TypeCheck n Bool
forall (n :: S). Distinct n => TypeCheck n Bool
contextEntailsBottom
  pure [ recBottomT | vacuous ]

-- | Whether the local tope context is covered by the union of the given topes — the
-- coverage obligation of @recOR@, as a yes\/no query rather than a check that
-- issues an error.
coverageHolds :: Distinct n => [TermT n] -> TypeCheck n Bool
coverageHolds :: forall (n :: S). Distinct n => [TermT n] -> TypeCheck n Bool
coverageHolds [TermT n]
topes = do
  topesNF <- (TermT n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (TermT n))
-> [TermT n]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
nfTope [TermT n]
topes
  entailContextM (foldr topeOrT topeBottomT topesNF)

-- | Tope case-split moves: ways to build a value of the goal by @recOR@, splitting
-- the proof over a cover of the local tope context. Three sources, offered together
-- (the UI ranks and filters):
--
--   * each disjunction @ψ ∨ φ@ already in the context becomes @recOR(ψ ↦ ?, φ ↦ ?)@
--     — its cover is immediate;
--   * when the goal is an extension type, its restriction faces are a cover
--     candidate, offered only when they actually cover the context (so the move
--     typechecks);
--   * a generic two-way split @recOR(? ↦ ?, ? ↦ ?)@ with the guards left as holes,
--     for an unusual split the player fills in by hand.
--
-- All three are offered only where a split makes sense — a cube variable is in
-- scope, the context has a non-trivial tope, or the goal is a restricted type — so
-- an ordinary (tope-free) goal is left alone.
recOrCandidates :: Distinct n => TermT n -> TypeCheck n [TermT n]
recOrCandidates :: forall (n :: S). Distinct n => TermT n -> TypeCheck n [TermT n]
recOrCandidates TermT n
goal = do
  goalW   <- TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TermT n
goal
  topes   <- asks (filter (not . eqT topeTopT) . availableTopes)
  locals  <- asks localHypotheses
  hasCube <- or <$> mapM (fmap isCubeType . whnfT . varType . snd) locals
  let stripped     = TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
stripTypeRestrictions TermT n
goalW
      mkRecOr [TermT n]
gs   = TermT n -> [(TermT n, TermT n)] -> TermT n
forall (n :: S). TermT n -> [(TermT n, TermT n)] -> TermT n
recOrT TermT n
stripped [ (TermT n
g, TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
stripped) | TermT n
g <- [TermT n]
gs ]
      fromContext  = [ [TermT n] -> TermT n
mkRecOr [TermT n
l, TermT n
r] | TopeOrT TypeInfo (TermT n)
_ TermT n
l TermT n
r <- [TermT n]
topes ]
      faces        = case TermT n
goalW of
        TypeRestrictedT TypeInfo (TermT n)
_ TermT n
_ [(TermT n, TermT n)]
rs -> ((TermT n, TermT n) -> TermT n)
-> [(TermT n, TermT n)] -> [TermT n]
forall a b. (a -> b) -> [a] -> [b]
map (TermT n, TermT n) -> TermT n
forall a b. (a, b) -> a
fst [(TermT n, TermT n)]
rs
        TermT n
_                      -> []
      isRestricted = case TermT n
goalW of TypeRestrictedT{} -> Bool
True; TermT n
_ -> Bool
False
      inShape      = Bool
hasCube Bool -> Bool -> Bool
|| Bool -> Bool
not ([TermT n] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TermT n]
topes) Bool -> Bool -> Bool
|| Bool
isRestricted
      generic      = [ TermT n -> [(TermT n, TermT n)] -> TermT n
forall (n :: S). TermT n -> [(TermT n, TermT n)] -> TermT n
recOrT TermT n
stripped [ (TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
forall (n :: S). TermT n
topeT, TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
stripped)
                                       , (TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
forall (n :: S). TermT n
topeT, TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
mkHole TermT n
stripped) ]
                     | Bool
inShape ]
  fromFaces <- if length faces >= 2
    then do covered <- coverageHolds faces
            pure [ mkRecOr faces | covered ]
    else pure []
  pure (fromContext <> fromFaces <> generic)

-- | The local hypotheses: everything in scope that is not a top-level entry.
localHypotheses :: Context n -> [(Foil.Name n, VarInfo n)]
localHypotheses :: forall (n :: S). Context n -> [(Name n, VarInfo n)]
localHypotheses = ((Name n, VarInfo n) -> Bool)
-> [(Name n, VarInfo n)] -> [(Name n, VarInfo n)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Name n, VarInfo n) -> Bool) -> (Name n, VarInfo n) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarInfo n -> Bool
forall (n :: S). VarInfo n -> Bool
varIsTopLevel (VarInfo n -> Bool)
-> ((Name n, VarInfo n) -> VarInfo n)
-> (Name n, VarInfo n)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name n, VarInfo n) -> VarInfo n
forall a b. (a, b) -> b
snd) ([(Name n, VarInfo n)] -> [(Name n, VarInfo n)])
-> (Context n -> [(Name n, VarInfo n)])
-> Context n
-> [(Name n, VarInfo n)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context n -> [(Name n, VarInfo n)]
forall (n :: S). Context n -> [(Name n, VarInfo n)]
varsInScope

-- | The allow-listed top-level lemmas a hole's candidate list may draw on.
lemmaHypotheses :: Context n -> [(Foil.Name n, VarInfo n)]
lemmaHypotheses :: forall (n :: S). Context n -> [(Name n, VarInfo n)]
lemmaHypotheses Context n
ctx =
  [ (Name n, VarInfo n)
entry
  | entry :: (Name n, VarInfo n)
entry@(Name n
_, VarInfo n
info) <- Context n -> [(Name n, VarInfo n)]
forall (n :: S). Context n -> [(Name n, VarInfo n)]
varsInScope Context n
ctx
  , VarInfo n -> Bool
forall (n :: S). VarInfo n -> Bool
varIsTopLevel VarInfo n
info
  , Just VarIdent
name <- [Binder -> Maybe VarIdent
binderName (VarInfo n -> Binder
forall (n :: S). VarInfo n -> Binder
varOrig VarInfo n
info)]
  , VarIdent
name VarIdent -> [VarIdent] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Context n -> [VarIdent]
forall (n :: S). Context n -> [VarIdent]
ctxHintLemmas Context n
ctx
  ]

-- * Moves must parse back

-- | The elaboration environment at the current position: every in-scope
-- entry contributes its source name — a pattern its leaves, as projection
-- chains over the variable it binds — and an inner binding wins, exactly
-- as the elaborator resolves an identifier written here. Kept as a table
-- so 'sourceResolvesTo' and 'parsesBackTo' share it.
positionTable :: Context n -> Map.Map VarIdent (Term n)
positionTable :: forall (n :: S). Context n -> Map VarIdent (Term n)
positionTable Context n
ctx = [(VarIdent, Term n)] -> Map VarIdent (Term n)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(VarIdent, Term n)] -> Map VarIdent (Term n))
-> [(VarIdent, Term n)] -> Map VarIdent (Term n)
forall a b. (a -> b) -> a -> b
$ [[(VarIdent, Term n)]] -> [(VarIdent, Term n)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  -- 'varsInScope' lists entries oldest first, and 'Map.fromList' keeps the
  -- last value per key, so an inner binding shadows an outer one.
  [ Binder -> Name n -> [(VarIdent, Term n)]
forall {n :: S}.
Binder
-> Name n -> [(VarIdent, AST NameBinder (AnnSig SrcPos TermSig) n)]
entryBindings (VarInfo n -> Binder
forall (n :: S). VarInfo n -> Binder
varOrig VarInfo n
info) Name n
v
  | (Name n
v, VarInfo n
info) <- Context n -> [(Name n, VarInfo n)]
forall (n :: S). Context n -> [(Name n, VarInfo n)]
varsInScope Context n
ctx
  ]
  where
    entryBindings :: Binder
-> Name n -> [(VarIdent, AST NameBinder (AnnSig SrcPos TermSig) n)]
entryBindings Binder
orig Name n
v = case Binder
orig of
      BinderVar (Just VarIdent
x) -> [(VarIdent
x, Name n -> AST NameBinder (AnnSig SrcPos TermSig) n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
v)]
      BinderVar Maybe VarIdent
Nothing  -> []
      Binder
BinderUnit         -> []
      Binder
b                  -> Pattern
-> AST NameBinder (AnnSig SrcPos TermSig) n
-> [(VarIdent, AST NameBinder (AnnSig SrcPos TermSig) n)]
forall (n :: S). Pattern -> Term n -> [(VarIdent, Term n)]
Convert.bindings (Binder -> Pattern
binderToPattern Binder
b) (Name n -> AST NameBinder (AnnSig SrcPos TermSig) n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
v)

-- | Does this variable's own source name, written at the current position,
-- resolve back to it?
sourceResolvesTo :: Map.Map VarIdent (Term n) -> VarIdent -> Foil.Name n -> Bool
sourceResolvesTo :: forall (n :: S).
Map VarIdent (Term n) -> VarIdent -> Name n -> Bool
sourceResolvesTo Map VarIdent (Term n)
table VarIdent
src Name n
v = case VarIdent -> Map VarIdent (Term n) -> Maybe (Term n)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VarIdent
src Map VarIdent (Term n)
table of
  Just (Var Name n
v') -> Name n -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name n
v' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Name n -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name n
v
  Maybe (Term n)
_             -> Bool
False

-- | Does a rendered move, inserted as source text at the current position,
-- parse and resolve back to the very term it renders? The comparison is
-- α-equivalence of the untyped skeletons: a move is well-typed by
-- construction, and insertion is a question of naming. This is the exact
-- form of the old referability guard, and it enforces the move contract
-- for everything emitted — a shadowing or unresolvable name anywhere in
-- the rendering shows up as a resolution difference and drops the move.
parsesBackTo
  :: Distinct n
  => Map.Map VarIdent (Term n) -> TermT n -> Rendered -> TypeCheck n Bool
parsesBackTo :: forall (n :: S).
Distinct n =>
Map VarIdent (Term n) -> TermT n -> Rendered -> TypeCheck n Bool
parsesBackTo Map VarIdent (Term n)
table TermT n
move Rendered
rendered = do
  ctx <- ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Context n)
forall r (m :: * -> *). MonadReader r m => m r
ask
  let scope = Context n -> Scope n
forall (n :: S). Context n -> Scope n
ctxScope Context n
ctx
      units = [Int] -> IntSet
IntSet.fromList
        [ Name n -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name n
v
        | (Name n
v, VarInfo n
info) <- Context n -> [(Name n, VarInfo n)]
forall (n :: S). Context n -> [(Name n, VarInfo n)]
varsInScope Context n
ctx
        , Binder
BinderUnit <- [VarInfo n -> Binder
forall (n :: S). VarInfo n -> Binder
varOrig VarInfo n
info]
        ]
      collapse = IntSet -> Term n -> Term n
forall (l :: S). IntSet -> Term l -> Term l
unitPointCollapse IntSet
units (Term n -> Term n) -> (Term n -> Term n) -> Term n -> Term n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scope n -> Term n -> Term n
forall (n :: S). Distinct n => Scope n -> Term n -> Term n
pairEtaCollapse Scope n
scope
      env VarIdent
name = Term n -> VarIdent -> Map VarIdent (Term n) -> Term n
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (Maybe VarIdent -> Term n
forall {n :: S}. Maybe VarIdent -> Term n
Hole (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just (VarIdent -> VarIdent
markUnresolved VarIdent
name))) VarIdent
name Map VarIdent (Term n)
table
  pure $ case Rzk.parseTerm (T.pack (show rendered)) of
    Left Text
_        -> Bool
False
    Right Term
surface ->
      Scope n -> Term n -> Term n -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope n
scope
        (Term n -> Term n
collapse (Scope n -> (VarIdent -> Term n) -> Term -> Term n
forall (n :: S). Distinct n => Scope n -> Env n -> Term -> Term n
Convert.toTerm Scope n
scope VarIdent -> Term n
env Term
surface))
        (Term n -> Term n
collapse (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
move))

-- | Collapse a literal pair of matching projections, recursively along the
-- pair spine: @(π₁ p, π₂ p)@ reads back as @p@. This is exactly what the
-- whole-point rendering of a pattern-bound variable parses to (the pattern
-- @(x, y)@ resolves to the projections), so the comparison in
-- 'parsesBackTo' absorbs the projection-folding convention.
pairEtaCollapse :: Distinct n => Foil.Scope n -> Term n -> Term n
pairEtaCollapse :: forall (n :: S). Distinct n => Scope n -> Term n -> Term n
pairEtaCollapse Scope n
scope Term n
t = case Term n
t of
  Pair Term n
l Term n
r ->
    case (Scope n -> Term n -> Term n
forall (n :: S). Distinct n => Scope n -> Term n -> Term n
pairEtaCollapse Scope n
scope Term n
l, Scope n -> Term n -> Term n
forall (n :: S). Distinct n => Scope n -> Term n -> Term n
pairEtaCollapse Scope n
scope Term n
r) of
      (First Term n
a, Second Term n
b) | Scope n -> Term n -> Term n -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope n
scope Term n
a Term n
b -> Term n
a
      (Term n
l', Term n
r')                                   -> Term n -> Term n -> Term n
forall {n :: S}. Term n -> Term n -> Term n
Pair Term n
l' Term n
r'
  Term n
_ -> Term n
t

-- | Collapse a variable bound by the unit pattern to the constructor. A
-- @\\ unit → …@ binds a point of @Unit@ whose whole-point rendering (and the
-- only way to write it) is @unit@, which parses back as the constructor. The
-- two are the same point of the singleton, so the comparison in
-- 'parsesBackTo' treats them as one, exactly as 'pairEtaCollapse' absorbs
-- the projection-folding convention.
unitPointCollapse :: IntSet.IntSet -> Term l -> Term l
unitPointCollapse :: forall (l :: S). IntSet -> Term l -> Term l
unitPointCollapse IntSet
units = Term l -> Term l
forall (x :: S). Term x -> Term x
go
  where
    go :: Term x -> Term x
    go :: forall (x :: S). Term x -> Term x
go t :: Term x
t@(Var Name x
x)
      | Name x -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name x
x Int -> IntSet -> Bool
`IntSet.member` IntSet
units = Term x
forall {n :: S}. Term n
Unit
      | Bool
otherwise                           = Term x
t
    go (Node AnnSig
  SrcPos
  TermSig
  (ScopedAST NameBinder (AnnSig SrcPos TermSig) x)
  (Term x)
sig) = AnnSig
  SrcPos
  TermSig
  (ScopedAST NameBinder (AnnSig SrcPos TermSig) x)
  (Term x)
-> Term x
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node ((ScopedAST NameBinder (AnnSig SrcPos TermSig) x
 -> ScopedAST NameBinder (AnnSig SrcPos TermSig) x)
-> (Term x -> Term x)
-> AnnSig
     SrcPos
     TermSig
     (ScopedAST NameBinder (AnnSig SrcPos TermSig) x)
     (Term x)
-> AnnSig
     SrcPos
     TermSig
     (ScopedAST NameBinder (AnnSig SrcPos TermSig) x)
     (Term x)
forall a b c d.
(a -> b)
-> (c -> d)
-> AnnSig SrcPos TermSig a c
-> AnnSig SrcPos TermSig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ScopedAST NameBinder (AnnSig SrcPos TermSig) x
-> ScopedAST NameBinder (AnnSig SrcPos TermSig) x
forall (x :: S). ScopedTerm x -> ScopedTerm x
goScoped Term x -> Term x
forall (x :: S). Term x -> Term x
go AnnSig
  SrcPos
  TermSig
  (ScopedAST NameBinder (AnnSig SrcPos TermSig) x)
  (Term x)
sig)

    goScoped :: ScopedTerm x -> ScopedTerm x
    goScoped :: forall (x :: S). ScopedTerm x -> ScopedTerm x
goScoped (ScopedAST NameBinder x l
b AST NameBinder (AnnSig SrcPos TermSig) l
body) = NameBinder x l
-> AST NameBinder (AnnSig SrcPos TermSig) l
-> ScopedAST NameBinder (AnnSig SrcPos TermSig) x
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder x l
b (AST NameBinder (AnnSig SrcPos TermSig) l
-> AST NameBinder (AnnSig SrcPos TermSig) l
forall (x :: S). Term x -> Term x
go AST NameBinder (AnnSig SrcPos TermSig) l
body)

-- | Record the goal and local context at a hole (lenient mode only).
recordHole :: Distinct n => Maybe VarIdent -> TermT n -> TypeCheck n ()
recordHole :: forall (n :: S).
Distinct n =>
Maybe VarIdent -> TermT n -> TypeCheck n ()
recordHole Maybe VarIdent
mname TermT n
goalTy = Maybe VarIdent
-> TermT n -> Maybe (Binder, ScopedTermT n) -> TypeCheck n ()
forall (n :: S).
Distinct n =>
Maybe VarIdent
-> TermT n -> Maybe (Binder, ScopedTermT n) -> TypeCheck n ()
recordHoleShape Maybe VarIdent
mname TermT n
goalTy Maybe (Binder, ScopedTermT n)
forall a. Maybe a
Nothing

-- | Record a hole. When the hole is the argument of a shape-restricted function its
-- goal is a /shape/: the cube @goalTy@ together with a membership tope, which is a
-- scope over the shape's bound variable. It is rendered under that binder, so the
-- goal reads @(binder : goalTy | tope)@.
recordHoleShape
  :: Distinct n
  => Maybe VarIdent
  -> TermT n
  -> Maybe (Binder, ScopedTermT n)
  -> TypeCheck n ()
recordHoleShape :: forall (n :: S).
Distinct n =>
Maybe VarIdent
-> TermT n -> Maybe (Binder, ScopedTermT n) -> TypeCheck n ()
recordHoleShape Maybe VarIdent
mname TermT n
goalTy Maybe (Binder, ScopedTermT n)
mshape = do
  goal'     <- TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TermT n
goalTy
  locals    <- asks localHypotheses
  -- named top-level lemmas the caller allow-listed for hints. They feed the
  -- candidate-elimination loop only — not the local context shown to the user,
  -- since they are global definitions, not local hypotheses.
  lemmaVars <- asks lemmaHypotheses
  -- a variable bound by the unit pattern is not a hypothesis the user named
  -- (the pattern binds nothing referable, and the point is spelled @unit@),
  -- so it is not shown in the context panel
  let shownLocals = [ (Name n, VarInfo n)
l | l :: (Name n, VarInfo n)
l@(Name n
_, VarInfo n
info) <- [(Name n, VarInfo n)]
locals, Bool -> Bool
not (Binder -> Bool
isUnitBinder (VarInfo n -> Binder
forall (n :: S). VarInfo n -> Binder
varOrig VarInfo n
info)) ]
      isUnitBinder Binder
BinderUnit = Bool
True
      isUnitBinder Binder
_          = Bool
False
  cubeFlags <- mapM (fmap isCubeType . whnfT . varType . snd) shownLocals
  topes     <- asks (filter (not . eqT topeTopT) . availableTopes)
  loc       <- asks ctxLocation
  naming    <- asks namingOfContext

  -- The one environment every move is built and judged against. The source
  -- namespace at the hole ('positionTable') is what 'parsesBackTo' checks
  -- the emitted text against. A binder a move introduces (a λ-introduction,
  -- an idJ motive's binders, a data eliminator's motive λs) is freshened
  -- against the union of that namespace with the display names of the
  -- local context: the former so an accepted move never shadows anything
  -- writable here, the latter so a move's binder never reads like a
  -- variable the context panel already shows under a refreshed name.
  ctx <- ask
  let table = Context n -> Map VarIdent (Term n)
forall (n :: S). Context n -> Map VarIdent (Term n)
positionTable Context n
ctx
      displayNames = [VarIdent] -> Set VarIdent
forall a. Ord a => [a] -> Set a
Set.fromList
        [ VarIdent
nm
        | (Name n
v, VarInfo n
_) <- [(Name n, VarInfo n)]
locals
        , VarIdent
nm <- case Naming n -> Name n -> Display
forall (n :: S). Naming n -> Name n -> Display
displayOf Naming n
naming Name n
v of
            (VarIdent
_, Binder
binder) | Binder -> Bool
binderIsCompound Binder
binder -> Binder -> [VarIdent]
binderLeaves Binder
binder
            (VarIdent
x, Binder
_)                                -> [VarIdent
x]
        ]
      takenNames = Map VarIdent (Term n) -> Set VarIdent
forall k a. Map k a -> Set k
Map.keysSet Map VarIdent (Term n)
table Set VarIdent -> Set VarIdent -> Set VarIdent
forall a. Semigroup a => a -> a -> a
<> Set VarIdent
displayNames

  -- for each local hypothesis (and allow-listed lemma), the elimination spines that
  -- land in the goal (arguments left as holes). Probing must not leak holes into the
  -- recorded output, hence the 'suppressing'.
  candidates <- suppressing $ do
    -- over the shown hypotheses: a unit-bound point admits no elimination,
    -- and offering it bare would duplicate the @unit@ introduction
    elims <- concat <$>
      mapM (\(Name n
v, VarInfo n
_) -> TermT n
-> Set VarIdent
-> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [TermT n]
forall (n :: S).
Distinct n =>
TermT n -> Set VarIdent -> TermT n -> TypeCheck n [TermT n]
allEliminationsInto TermT n
goalTy Set VarIdent
takenNames (Name n -> TermT n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
v)) (shownLocals ++ lemmaVars)
    -- context-driven moves (independent of the goal's head and the hypotheses): ex
    -- falso in a contradictory context, and tope case-splits. recOR and recBOT are
    -- term-level eliminators, so they are offered only for a term goal — not when
    -- the hole is a cube point or a tope, where they cannot appear.
    let termLayer = Bool -> Bool
not (TermT n -> Bool
forall (n :: S). TermT n -> Bool
isCubeOrTopeType TermT n
goal')
    recbot <- if termLayer then recBottomCandidates    else pure []
    recor  <- if termLayer then recOrCandidates goalTy else pure []
    pure (elims <> recbot <> recor)

  -- A move is inserted as source text, so it is rendered with source names
  -- wherever they still resolve (an inner @b@ beside a shadowed outer @b@
  -- renders as @b@, not as its display name @b₁@), and it is emitted only
  -- if the rendered text parses back, at this position, to the very term
  -- it renders ('parsesBackTo'). The display naming is unchanged: the
  -- context panel keeps its refreshed names.
  let moveNaming = Naming n
naming
        { namingOf = NameMap (IntMap.fromList
            [ (Foil.nameId v, fixed)
            | (v, info) <- varsInScope ctx
            , let fixed = case Binder -> Maybe VarIdent
binderName (VarInfo n -> Binder
forall (n :: S). VarInfo n -> Binder
varOrig VarInfo n
info) of
                    Just VarIdent
src | Map VarIdent (Term n) -> VarIdent -> Name n -> Bool
forall (n :: S).
Map VarIdent (Term n) -> VarIdent -> Name n -> Bool
sourceResolvesTo Map VarIdent (Term n)
table VarIdent
src Name n
v ->
                      (VarIdent
src, Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
src))
                    Maybe VarIdent
_ -> Naming n -> Name n -> Display
forall (n :: S). Naming n -> Name n -> Display
displayOf Naming n
naming Name n
v
            ]) }
      renderMove TermT n
t = Naming n -> Term n -> Rendered
forall (n :: S). Naming n -> Term n -> Rendered
renderTerm Naming n
moveNaming (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
t)
  candidateMoves <- fmap concat $ forM candidates $ \TermT n
c -> do
    let r :: Rendered
r = TermT n -> Rendered
renderMove TermT n
c
    ok <- Map VarIdent (Term n)
-> TermT n
-> Rendered
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall (n :: S).
Distinct n =>
Map VarIdent (Term n) -> TermT n -> Rendered -> TypeCheck n Bool
parsesBackTo Map VarIdent (Term n)
table TermT n
c Rendered
r
    pure [ r | ok ]

  let render TermT n
t = Naming n -> Term n -> Rendered
forall (n :: S). Naming n -> Term n -> Rendered
renderTerm Naming n
naming (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
t)
      -- a pattern binder is shown as its pattern, e.g. (t , s); others by name
      entryName Name n
v = case Naming n -> Name n -> Display
forall (n :: S). Naming n -> Name n -> Display
displayOf Naming n
naming Name n
v of
        (VarIdent
_, Binder
binder) | Binder -> Bool
binderIsCompound Binder
binder -> Binder -> VarIdent
binderDisplayName Binder
binder
        (VarIdent
x, Binder
_)                                -> VarIdent
x
      entries = [ VarIdent -> Rendered -> HoleEntry
HoleEntry (Name n -> VarIdent
entryName Name n
v) (TermT n -> Rendered
render (VarInfo n -> TermT n
forall (n :: S). VarInfo n -> TermT n
varType VarInfo n
info)) | (Name n
v, VarInfo n
info) <- [(Name n, VarInfo n)]
shownLocals ]
      flagged = [Bool] -> [HoleEntry] -> [(Bool, HoleEntry)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Bool]
cubeFlags [HoleEntry]
entries

  -- The goal shape, rendered under the shape's own binder. The name is read back
  -- from the naming rather than assumed: if the declared name is taken (the goal
  -- @(t : 2 × 2 | Δ¹×Δ¹ t)@ under an enclosing @t@), the binder is refreshed, and
  -- the tope must be shown under the /same/ name it is.
  goalShape <- forM mshape $ \(Binder
orig, ScopedTermT n
tope) ->
    Binder
-> TModality
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l (VarIdent, Rendered))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (VarIdent, Rendered)
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l a)
-> TypeCheck n a
withBinder (Maybe VarIdent -> Binder
BinderVar (Binder -> Maybe VarIdent
binderName Binder
orig Maybe VarIdent -> Maybe VarIdent -> Maybe VarIdent
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
"t")) TModality
Id TermT n
goal' ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> TypeCheck l (VarIdent, Rendered))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (VarIdent, Rendered))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l (VarIdent, Rendered))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (VarIdent, Rendered)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder -> do
      topeAt <- NameBinder n l
-> ScopedTermT n
-> TypeCheck l (AST NameBinder (AnnSig TypeInfo TermSig) l)
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
NameBinder n l
-> ScopedAST NameBinder sig n -> TypeCheck l (AST NameBinder sig l)
openScoped NameBinder n l
binder ScopedTermT n
tope
      naming' <- asks namingOfContext
      let (shapeBinder, _) = displayOf naming' (Foil.nameOf binder)
      pure (shapeBinder, renderTerm naming' (untyped topeAt))

  -- the introduction forms for the goal itself (constituents left as holes); the Π
  -- binder is freshened against the names in scope so that it does not shadow,
  -- and the parse-back check applies like it does to the candidates.
  introductions <- suppressing (allIntroductionsOf goalTy takenNames)
  introductionMoves <- fmap concat $ forM introductions $ \TermT n
i -> do
    let r :: Rendered
r = TermT n -> Rendered
renderMove TermT n
i
    ok <- Map VarIdent (Term n)
-> TermT n
-> Rendered
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall (n :: S).
Distinct n =>
Map VarIdent (Term n) -> TermT n -> Rendered -> TypeCheck n Bool
parsesBackTo Map VarIdent (Term n)
table TermT n
i Rendered
r
    pure [ r | ok ]
  -- the goal cell: an SVG of the shape the hole must inhabit (an arrow, triangle or
  -- square), drawn from an abstract inhabitant with the proof term hidden. 'Nothing'
  -- when the goal is not a renderable shape.
  diagram <- suppressing (renderGoalCellSVG goal')

  recordHoleInfo HoleInfo
    { holeName          = mname
    , holeGoal          = render goal'
    , holeGoalShape     = goalShape
    , holeTermVars      = [ e | (False, e) <- flagged ]
    , holeCubeVars      = [ e | (True,  e) <- flagged ]
    , holeTopes         = map render topes
    , holeCandidates    = candidateMoves
    , holeIntroductions = introductionMoves
    , holeDiagram       = diagram
    , holeLocation      = loc
    }

-- | Check a hole that appears as the argument of a shape-restricted function, whose
-- domain is the cube @cube@ restricted by @tope@ (a scope over the domain's bound
-- variable). Mirrors the hole case of 'typecheck', but records the shape as the
-- hole's goal so the diagnostic shows @(binder : cube | tope)@.
checkHoleAgainstShape
  :: Distinct n
  => Maybe VarIdent -> Binder -> TermT n -> ScopedTermT n
  -> TypeCheck n (TermT n)
checkHoleAgainstShape :: forall (n :: S).
Distinct n =>
Maybe VarIdent
-> Binder -> TermT n -> ScopedTermT n -> TypeCheck n (TermT n)
checkHoleAgainstShape Maybe VarIdent
mname Binder
orig TermT n
cube ScopedTermT n
tope = do
  reject <- (Context n -> Bool)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context n -> Bool
forall (n :: S). Context n -> Bool
ctxHolesAreErrors
  if reject
    then issueTypeError (TypeErrorUnsolvedHole mname cube)
    else do
      recordHoleShape mname cube (Just (orig, tope))
      pure (holeT cube mname)


-- * Checking

-- | Check a @recOR@ against a known expected type: each branch is checked against
-- it under its own guard, the branches must agree on their overlaps, and together
-- they must cover the context.
checkRecOrAgainst
  :: Distinct n => TermT n -> [(Term n, Term n)] -> TypeCheck n (TermT n)
checkRecOrAgainst :: forall (n :: S).
Distinct n =>
TermT n -> [(Term n, Term n)] -> TypeCheck n (TermT n)
checkRecOrAgainst TermT n
expected [(Term n, Term n)]
rs = do
  rs' <- [(Term n, Term n)]
-> ((Term n, Term n)
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (TermT n, TermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(TermT n, TermT n)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Term n, Term n)]
rs (((Term n, Term n)
  -> ReaderT
       (Context n)
       (ExceptT TypeErrorInScopedContext (State CheckLog))
       (TermT n, TermT n))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [(TermT n, TermT n)])
-> ((Term n, Term n)
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (TermT n, TermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(TermT n, TermT n)]
forall a b. (a -> b) -> a -> b
$ \(Term n
tope, Term n
rterm) -> do
    tope' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
tope TermT n
forall (n :: S). TermT n
topeT
    checkTopeAgainstContext "recOR branch guard" tope'
    localTope tope' $ do
      expected' <- pruneVacuousFaces expected
      rterm' <- typecheck rterm expected'
      return (tope', rterm')
  sequence_ [ checkCoherence l r | l:rs'' <- tails rs', r <- rs'' ]
  contextEntailsUnion (map fst rs')
  return (recOrT expected rs')

-- | Drop the restriction faces of an extension type that are vacuous in the current
-- tope context (their overlap with the context is the empty tope ⊥). A face
-- mentioning an unfilled hole cannot be decided, so it is kept. Non-extension types
-- are returned unchanged. Used when descending into a recOR branch, where the
-- sibling branches' faces are disjoint from the branch guard.
pruneVacuousFaces :: Distinct n => TermT n -> TypeCheck n (TermT n)
pruneVacuousFaces :: forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
pruneVacuousFaces (TypeRestrictedT TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
_info AST NameBinder (AnnSig TypeInfo TermSig) n
ty [(AST NameBinder (AnnSig TypeInfo TermSig) n,
  AST NameBinder (AnnSig TypeInfo TermSig) n)]
rs) = do
  contextTopes <- (Context n -> [ModalTope n])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [ModalTope n]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context n -> [ModalTope n]
forall (n :: S). Context n -> [ModalTope n]
ctxTopesNF
  kept <- fmap concat $ forM rs $ \face :: (AST NameBinder (AnnSig TypeInfo TermSig) n,
 AST NameBinder (AnnSig TypeInfo TermSig) n)
face@(AST NameBinder (AnnSig TypeInfo TermSig) n
tope, AST NameBinder (AnnSig TypeInfo TermSig) n
_) -> do
    vacuous <- if AST NameBinder (AnnSig TypeInfo TermSig) n -> Bool
forall (n :: S). TermT n -> Bool
containsHole AST NameBinder (AnnSig TypeInfo TermSig) n
tope
      then Bool
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      else (AST NameBinder (AnnSig TypeInfo TermSig) n -> ModalTope n
forall (n :: S). TermT n -> ModalTope n
plainTope AST NameBinder (AnnSig TypeInfo TermSig) n
tope ModalTope n -> [ModalTope n] -> [ModalTope n]
forall a. a -> [a] -> [a]
: [ModalTope n]
contextTopes) [ModalTope n]
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall (n :: S).
Distinct n =>
[ModalTope n] -> TermT n -> TypeCheck n Bool
`entailM` AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
topeBottomT
    return [ face | not vacuous ]
  return $ case kept of
    [] -> AST NameBinder (AnnSig TypeInfo TermSig) n
ty
    [(AST NameBinder (AnnSig TypeInfo TermSig) n,
  AST NameBinder (AnnSig TypeInfo TermSig) n)]
_  -> AST NameBinder (AnnSig TypeInfo TermSig) n
-> [(AST NameBinder (AnnSig TypeInfo TermSig) n,
     AST NameBinder (AnnSig TypeInfo TermSig) n)]
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n -> [(TermT n, TermT n)] -> TermT n
typeRestrictedT AST NameBinder (AnnSig TypeInfo TermSig) n
ty [(AST NameBinder (AnnSig TypeInfo TermSig) n,
  AST NameBinder (AnnSig TypeInfo TermSig) n)]
kept
pruneVacuousFaces AST NameBinder (AnnSig TypeInfo TermSig) n
ty = AST NameBinder (AnnSig TypeInfo TermSig) n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return AST NameBinder (AnnSig TypeInfo TermSig) n
ty

typecheck :: Distinct n => Term n -> TermT n -> TypeCheck n (TermT n)
typecheck :: forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
term TermT n
ty = Action n -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) a.
Distinct n =>
Action n -> TypeCheck n a -> TypeCheck n a
performing (Term n -> TermT n -> Action n
forall (n :: S). Term n -> TermT n -> Action n
ActionTypeCheck Term n
term TermT n
ty) (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ case Term n
term of
  -- An identifier that was not in scope: elaboration marked it, and this is where
  -- it is reported, under the binders and topes it was written beneath.
  Hole (Just VarIdent
name) | Just VarIdent
x <- VarIdent -> Maybe VarIdent
unmarkUnresolved VarIdent
name ->
    TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (VarIdent -> TypeError n
forall (n :: S). VarIdent -> TypeError n
TypeErrorUndefined VarIdent
x)

  -- A hole is checked against a known type (this is checking position): in strict
  -- mode it is reported as an unsolved hole; in lenient mode its goal and context
  -- are recorded and it is treated as inhabiting the expected type.
  Hole Maybe VarIdent
mname -> do
    reject <- (Context n -> Bool)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context n -> Bool
forall (n :: S). Context n -> Bool
ctxHolesAreErrors
    if reject
      then issueTypeError (TypeErrorUnsolvedHole mname ty)
      else do
        recordHole mname ty
        return (holeT ty mname)

  Term n
_ -> TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TermT n
ty TypeCheck n (TermT n)
-> (TermT n -> TypeCheck n (TermT n)) -> TypeCheck n (TermT n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case

    RecBottomT{} -> do
      -- Even under an absurd tope context (where the expected type collapses to
      -- recBOT), the term must still be well-formed in its own right, so that
      -- ill-typed bodies are not silently admitted under a false hypothesis. We
      -- synthesise its type, discard the result, and keep the recBOT elaboration.
      _ <- Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
term
      return recBottomT

    tr :: TermT n
tr@(TypeRestrictedT TypeInfo (TermT n)
_ty TermT n
ty' [(TermT n, TermT n)]
rs) -> case Term n
term of
      -- A recOR against a restricted type: push the restriction into each branch
      -- rather than stripping it first, so that a branch hole reports the boundary
      -- faces it must satisfy under its guard tope, and not the bare underlying
      -- type. Concrete branches still meet the faces, which are checked on each
      -- branch's overlap with them (see the general case below).
      RecOr [(Term n, Term n)]
branches -> TermT n -> [(Term n, Term n)] -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
TermT n -> [(Term n, Term n)] -> TypeCheck n (TermT n)
checkRecOrAgainst TermT n
tr [(Term n, Term n)]
branches
      Term n
_ -> do
        term' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
term TermT n
ty'
        -- NOTE: restriction faces need not be contained in the local tope context.
        -- Each face is checked only on its overlap with the context, so an
        -- overhanging face is harmless (we only hint); a face disjoint from the
        -- context is vacuous, however, and is an error.
        forM_ rs $ \(TermT n
tope, TermT n
rterm) -> do
          String -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => String -> TermT n -> TypeCheck n ()
checkTopeAgainstContext String
"restriction face" TermT n
tope
          TermT n -> TypeCheck n () -> TypeCheck n ()
forall (n :: S) a.
Distinct n =>
TermT n -> TypeCheck n a -> TypeCheck n a
localTope TermT n
tope (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$
            TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTerms TermT n
rterm TermT n
term'
        return term'    -- FIXME: correct?

    TermT n
ty' -> case Term n
term of
      Lambda Binder
orig Maybe (LambdaParam (ScopedTerm n) (Term n))
mparam ScopedTerm n
body ->
        case TermT n
ty' of
          TypeFunT TypeInfo (TermT n)
_ty Binder
_orig' TModality
md' TermT n
param' Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope' ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret -> do
            -- The λ's own domain annotation, if it wrote one, must agree with the
            -- domain of the type it is checked against.
            case Maybe (LambdaParam (ScopedTerm n) (Term n))
mparam of
              Maybe (LambdaParam (ScopedTerm n) (Term n))
Nothing -> () -> TypeCheck n ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

              Just (LambdaParam TModality
md Term n
param Maybe (ScopedTerm n)
Nothing) -> do
                Bool -> TypeCheck n () -> TypeCheck n ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TModality
md TModality -> TModality -> Bool
forall a. Eq a => a -> a -> Bool
/= TModality
md') (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$
                  TypeError n -> TypeCheck n ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TModality -> TModality -> Term n -> TypeError n
forall (n :: S). TModality -> TModality -> Term n -> TypeError n
TypeErrorModalityMismatch TModality
md' TModality
md Term n
term)
                paramType <- TModality -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
md (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
param
                -- an argument can be a shape, which is a function into TOPE; the
                -- domain is then its cube, and its tope is the λ's shape tope.
                mcube <- typeOf paramType >>= \case
                  TypeFunT TypeInfo (TermT n)
_ty Binder
_orig TModality
_md TermT n
cube Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_mtope (ScopedAST NameBinder n l
_ UniverseTopeT{}) -> do
                    (VarIdent -> TypeCheck n ()) -> [VarIdent] -> TypeCheck n ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VarIdent -> TypeCheck n ()
forall (n :: S). VarIdent -> TypeCheck n ()
checkNameShadowing (Binder -> [VarIdent]
binderLeaves Binder
orig)
                    Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
cube)
                  TermT n
_kind -> Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (TermT n)
forall a. Maybe a
Nothing
                unifyTerms param' (fromMaybe paramType mcube)
                mapM_ checkNameShadowing (binderLeaves orig)
                case mcube of
                  Maybe (TermT n)
Nothing -> () -> TypeCheck n ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  Just TermT n
_ ->
                    Binder
-> TModality
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l ())
-> TypeCheck n ()
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l a)
-> TypeCheck n a
withBinder Binder
orig TModality
md TermT n
param' ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> TypeCheck l ())
 -> TypeCheck n ())
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l ())
-> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder -> do
                      -- eta expand the shape into a tope over the bound variable
                      let etaTope :: TermT l
etaTope = TermT l -> TermT l -> TermT l -> TermT l
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT TermT l
forall (n :: S). TermT n
topeT (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
paramType) (Name l -> TermT l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder))
                      expected <- ReaderT
  (Context l)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (TermT l)
-> (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
    -> ReaderT
         (Context l)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (TermT l))
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT l)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TermT l
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT l)
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT l
forall (n :: S). TermT n
topeTopT) (NameBinder n l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT l)
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
NameBinder n l
-> ScopedAST NameBinder sig n -> TypeCheck l (AST NameBinder sig l)
openScoped NameBinder n l
binder) Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope'
                      unifyTerms expected etaTope

              Just (LambdaParam TModality
md Term n
param (Just ScopedTerm n
tope)) -> do
                Bool -> TypeCheck n () -> TypeCheck n ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TModality
md TModality -> TModality -> Bool
forall a. Eq a => a -> a -> Bool
/= TModality
md') (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$
                  TypeError n -> TypeCheck n ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TModality -> TModality -> Term n -> TypeError n
forall (n :: S). TModality -> TModality -> Term n -> TypeError n
TypeErrorModalityMismatch TModality
md' TModality
md Term n
term)
                param'' <- TModality -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
md (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
param (TermT n -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
param'
                unifyTerms param' param''
                mapM_ checkNameShadowing (binderLeaves orig)
                checkUnder orig md param' tope $ \NameBinder n l
binder Term l
topeTerm -> do
                  tope'' <- Term l -> TermT l -> TypeCheck l (TermT l)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term l
topeTerm TermT l
forall (n :: S). TermT n
topeT
                  expected <- maybe (pure topeTopT) (openScoped binder) mtope'
                  unifyTerms expected tope''

            (VarIdent -> TypeCheck n ()) -> [VarIdent] -> TypeCheck n ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VarIdent -> TypeCheck n ()
forall (n :: S). VarIdent -> TypeCheck n ()
checkNameShadowing (Binder -> [VarIdent]
binderLeaves Binder
orig)
            body' <- Binder
-> TModality
-> TermT n
-> Maybe (TermT n)
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l (TermT l))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
forall (n :: S).
Distinct n =>
Binder
-> TModality
-> TermT n
-> Maybe (TermT n)
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l (TermT l))
-> TypeCheck n (ScopedTermT n)
elaborateUnder Binder
orig TModality
md' TermT n
param' Maybe (TermT n)
forall a. Maybe a
Nothing ScopedTerm n
body ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> Term l -> TypeCheck l (TermT l))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l (TermT l))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder Term l
bodyTerm -> do
              mtopeIn <- (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
 -> TypeCheck l (TermT l))
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse (NameBinder n l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TypeCheck l (TermT l)
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
NameBinder n l
-> ScopedAST NameBinder sig n -> TypeCheck l (AST NameBinder sig l)
openScoped NameBinder n l
binder) Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope'
              maybe id localTope mtopeIn $ do
                retIn <- openScoped binder ret
                typecheck bodyTerm retIn
            return (lambdaT ty' orig (Just (LambdaParam md' param' mtope')) body')

          TermT n
_ -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TermT n -> TypeError n
forall (n :: S). Term n -> TermT n -> TypeError n
TypeErrorUnexpectedLambda Term n
term TermT n
ty

      Let Binder
orig Maybe (Term n)
annot Term n
val ScopedTerm n
body -> do
        val' <- Action n -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) a.
Distinct n =>
Action n -> TypeCheck n a -> TypeCheck n a
performing (Maybe VarIdent -> Action n
forall (n :: S). Maybe VarIdent -> Action n
ActionCheckLetValue (Binder -> Maybe VarIdent
binderName Binder
orig)) (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ case Maybe (Term n)
annot of
          Maybe (Term n)
Nothing -> Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
val
          Just Term n
bindType -> do
            bindType' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
bindType TermT n
forall (n :: S). TermT n
universeT
            typecheck val bindType'
        bindTy <- typeOf val'
        body' <- elaborateUnder orig Id bindTy (Just val') body $ \NameBinder n l
_binder Term l
bodyTerm ->
          Term l -> TermT l -> TypeCheck l (TermT l)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term l
bodyTerm (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
ty')
        return (letT ty' orig (Just bindTy) val' body')

      -- Only a motive-free @let mod@ is checked here: with no motive the body may
      -- be checked directly against the (sunk) goal. An explicit motive instead
      -- fixes the type of the whole let, so that form falls through to the generic
      -- branch below, which infers it and unifies the result against the goal.
      LetMod Binder
orig TModality
app TModality
inn Maybe (Term n)
annot Maybe (Term n)
Nothing Term n
val ScopedTerm n
body -> do
        val' <- Action n -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) a.
Distinct n =>
Action n -> TypeCheck n a -> TypeCheck n a
performing (Maybe VarIdent -> Action n
forall (n :: S). Maybe VarIdent -> Action n
ActionCheckLetValue (Binder -> Maybe VarIdent
binderName Binder
orig)) (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ case Maybe (Term n)
annot of
          Maybe (Term n)
Nothing -> TModality -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
app (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
val
          Just Term n
bindType -> do
            bindType' <- Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
bindType
            bindUniv <- typeOf bindType'
            enterModality app $ typecheck val (typeModalT bindUniv inn bindType')
        bindTy <- typeOf val' >>= \case
          o :: TermT n
o@(TypeModalT TypeInfo (TermT n)
_ty TModality
md TermT n
t) ->
            if TModality
md TModality -> TModality -> Bool
forall a. Eq a => a -> a -> Bool
== TModality
inn
              then TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return TermT n
t
              else TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TModality -> TermT n -> TypeError n
forall (n :: S). Term n -> TModality -> TermT n -> TypeError n
TypeErrorNotModal (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
o) TModality
inn TermT n
val'
          TermT n
o -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TModality -> TermT n -> TypeError n
forall (n :: S). Term n -> TModality -> TermT n -> TypeError n
TypeErrorNotModal (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
o) TModality
inn TermT n
val'
        bindVal <- whnfT val' >>= \case
          ModAppT TypeInfo (TermT n)
_ty TModality
_m TermT n
t -> Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
t)
          TermT n
o | TModality -> Bool
forall m. ModeTheory m => m -> Bool
isRA TModality
inn -> Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just (TermT n -> TModality -> TModality -> TermT n -> TermT n
forall (n :: S).
TermT n -> TModality -> TModality -> TermT n -> TermT n
modExtractT TermT n
bindTy TModality
app TModality
inn TermT n
o))
          TermT n
_ -> Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (TermT n)
forall a. Maybe a
Nothing
        body' <- elaborateUnder orig (comp app inn) bindTy bindVal body $ \NameBinder n l
_binder Term l
bodyTerm ->
          Term l -> TermT l -> TypeCheck l (TermT l)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term l
bodyTerm (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
ty')
        return (letModT ty' orig app inn (Just bindTy) Nothing val' body')

      Pair Term n
l Term n
r ->
        case TermT n
ty' of
          CubeProductT TypeInfo (TermT n)
_ty TermT n
a TermT n
b -> do
            l' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
l TermT n
a
            r' <- typecheck r b
            return (pairT ty' l' r')
          TypeSigmaT TypeInfo (TermT n)
_ty Binder
_orig TModality
md TermT n
a ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
b -> do
            l' <- TModality -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
md (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
l TermT n
a
            bAt <- instantiate b l'
            r' <- typecheck r bAt
            return (pairT ty' l' r')
          TermT n
_ -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TermT n -> TypeError n
forall (n :: S). Term n -> TermT n -> TypeError n
TypeErrorUnexpectedPair Term n
term TermT n
ty

      Refl Maybe (Term n, Maybe (Term n))
mx ->
        case TermT n
ty' of
          TypeIdT TypeInfo (TermT n)
_ty TermT n
y Maybe (TermT n)
_tA TermT n
z -> do
            tA <- TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
y
            forM_ mx $ \(Term n
x, Maybe (Term n)
mxty) -> do
              Maybe (Term n) -> (Term n -> TypeCheck n ()) -> TypeCheck n ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Maybe (Term n)
mxty ((Term n -> TypeCheck n ()) -> TypeCheck n ())
-> (Term n -> TypeCheck n ()) -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ \Term n
xty -> do
                xty' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
xty TermT n
forall (n :: S). TermT n
universeT
                unifyTerms tA xty'
              x' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
x TermT n
tA
              unifyTerms x' y >> unifyTerms y x'
              unifyTerms x' z >> unifyTerms z x'
            when (isNothing mx) $
              unifyTerms y z >> unifyTerms z y
            return (reflT ty' (Just (y, Just tA)))
          TermT n
_ -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TermT n -> TypeError n
forall (n :: S). Term n -> TermT n -> TypeError n
TypeErrorUnexpectedRefl Term n
term TermT n
ty

      ModExtract{} -> String -> TypeCheck n (TermT n)
forall a. String -> a
panicImpossible String
"extract is an internal term and cannot be typechecked"

      ModApp TModality
md Term n
body -> case TermT n
ty' of
        TypeModalT TypeInfo (TermT n)
_ty TModality
md' TermT n
tpe -> do
          Bool -> TypeCheck n () -> TypeCheck n ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TModality
md TModality -> TModality -> Bool
forall a. Eq a => a -> a -> Bool
/= TModality
md') (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ TypeError n -> TypeCheck n ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n ()) -> TypeError n -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$
            TModality -> TModality -> Term n -> TypeError n
forall (n :: S). TModality -> TModality -> Term n -> TypeError n
TypeErrorModalityMismatch TModality
md' TModality
md Term n
term
          body' <- TModality -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
md (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
body TermT n
tpe
          return $ modAppT ty' md body'
        TermT n
_ -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TModality -> TermT n -> TypeError n
forall (n :: S). Term n -> TModality -> TermT n -> TypeError n
TypeErrorNotModal Term n
term TModality
md TermT n
ty'

      -- In checking position the common type is already known, so we push it into
      -- every branch instead of inferring each one and unifying. This is what lets a
      -- bare hole branch (recOR(φ ↦ ?, …)) be checked against the expected type and
      -- recorded, rather than hitting TypeErrorCannotInferHole via the inference
      -- rule. A recOR is a term-level eliminator, not a tope; rejecting it when it is
      -- checked against the tope universe keeps it out of the tope layer, where it
      -- would otherwise hit a panic.
      RecOr [(Term n, Term n)]
rs -> case TermT n
ty' of
        UniverseTopeT{} -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$
          String -> TypeError n
forall (n :: S). String -> TypeError n
TypeErrorOther String
"a recOR cannot be used as a tope"
        TermT n
_ -> TermT n -> [(Term n, Term n)] -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
TermT n -> [(Term n, Term n)] -> TypeCheck n (TermT n)
checkRecOrAgainst TermT n
ty' [(Term n, Term n)]
rs

      Match Term n
scrut Maybe (Term n)
mmotive [(VarIdent, Term n)]
branches -> Term n
-> Term n
-> Maybe (Term n)
-> [(VarIdent, Term n)]
-> Maybe (TermT n)
-> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n
-> Term n
-> Maybe (Term n)
-> [(VarIdent, Term n)]
-> Maybe (TermT n)
-> TypeCheck n (TermT n)
checkMatch Term n
term Term n
scrut Maybe (Term n)
mmotive [(VarIdent, Term n)]
branches (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
ty')

      -- A neutral term is inferred, then its type unified with the expected one. In
      -- lenient (hole-checking) mode a term that still carries an unfilled hole is a
      -- work in progress, so a failure of that final unification is tolerated: the
      -- holes recorded while inferring the term stand, and we accept the term rather
      -- than rejecting the whole sketch. The mismatch is typically incidental to the
      -- missing pieces — an extension-type boundary face that only fails to line up
      -- because an argument hole sits in the wrong place (@f t@ vs @x@), where
      -- neither side is itself a hole, so the per-term deferral in unification cannot
      -- see it. Strict mode (the default, and CI) still rejects the mismatch.
      Term n
_ -> do
        term' <- Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
term
        inferredType <- typeOf term'
        lenient <- not <$> asks ctxHolesAreErrors
        if lenient && containsHole term'
          then unifyTypes term' ty' inferredType `catchError` \TypeErrorInScopedContext
_ -> () -> TypeCheck n ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          else unifyTypes term' ty' inferredType
        return term'

-- | How a match elaborates: which eliminator it targets, and — for @ind-D@ —
-- which variable scrutinee (if any) to abstract out of the goal when building
-- the motive. Computed once from the @into@ motive, the goal, and the
-- scrutinee, so that the eliminator choice and the later motive construction
-- read from the same decision instead of re-deriving it in two places.
data MatchPlan n
  = MatchRec
    -- ^ @rec-D@: a non-dependent family, so the motive has no scrutinee binder.
  | MatchInd (Maybe (Foil.Name n))
    -- ^ @ind-D@; the name, when present, is the variable scrutinee to abstract
    -- out of the goal.

-- | Elaborate a match into an application of its datatype's induction
-- eliminator: @ind-D params motive method₁ … methodₖ indices scrutinee@. The
-- spine is the result — a match node never survives elaboration (see the
-- ι-rule in "Rzk.TypeCheck.Eval" for how the spine then computes).
--
-- The motive is the elaborated @into@ term when one was written; otherwise it
-- is built from the goal, abstracting a variable scrutinee out of it (a
-- non-variable scrutinee gives a constant family). Without @into@ and without
-- a goal (inference position) the match is rejected.
checkMatch
  :: Distinct n
  => Term n                 -- ^ the whole match, for error messages
  -> Term n                 -- ^ the scrutinee
  -> Maybe (Term n)         -- ^ the @into@ motive, if written
  -> [(VarIdent, Term n)]   -- ^ branches: constructor name, arm chain
  -> Maybe (TermT n)        -- ^ the goal, in checking position
  -> TypeCheck n (TermT n)
checkMatch :: forall (n :: S).
Distinct n =>
Term n
-> Term n
-> Maybe (Term n)
-> [(VarIdent, Term n)]
-> Maybe (TermT n)
-> TypeCheck n (TermT n)
checkMatch Term n
term Term n
scrut Maybe (Term n)
mmotive [(VarIdent, Term n)]
branches Maybe (TermT n)
mgoal = do
  scrut' <- Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
scrut
  scrutTy <- stripTypeRestrictions <$> (typeOf scrut' >>= whnfT)
  d <- case collectAppSpine scrutTy of
    (Var Name n
d, [(TypeInfo (TermT n), TermT n)]
_) -> Name n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Name n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name n
d
    (TermT n, [(TypeInfo (TermT n), TermT n)])
_          -> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Name n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TermT n -> TermT n -> TypeError n
forall (n :: S). TermT n -> TermT n -> TypeError n
TypeErrorMatchScrutineeNotData TermT n
scrut' TermT n
scrutTy)
  elims <- dataEliminatorsOf d
  -- The eliminator to elaborate into: @ind-D@ when the motive genuinely
  -- depends on the scrutinee (an @into@ motive, or a variable scrutinee
  -- occurring in the goal); @rec-D@ otherwise. The choice matters for path
  -- constructors: under @rec-D@ a path branch is checked against the plain
  -- equation between the point branches, where @ind-D@ with a constant
  -- family would demand a transport that does not reduce.
  let plan = case (Maybe (Term n)
mmotive, Maybe (TermT n)
mgoal) of
        (Just Term n
_, Maybe (TermT n)
_)    -> Maybe (Name n) -> MatchPlan n
forall (n :: S). Maybe (Name n) -> MatchPlan n
MatchInd Maybe (Name n)
forall a. Maybe a
Nothing
        (Maybe (Term n)
_, Maybe (TermT n)
Nothing)   -> Maybe (Name n) -> MatchPlan n
forall (n :: S). Maybe (Name n) -> MatchPlan n
MatchInd Maybe (Name n)
forall a. Maybe a
Nothing
        (Maybe (Term n)
_, Just TermT n
goal) -> case TermT n
scrut' of
          Var Name n
v | Name n
v Name n -> [Name n] -> Bool
forall (n :: S). Name n -> [Name n] -> Bool
`elemName` TermT n -> [Name n]
forall (n :: S). TermT n -> [Name n]
freeVarsOfTermT TermT n
goal -> Maybe (Name n) -> MatchPlan n
forall (n :: S). Maybe (Name n) -> MatchPlan n
MatchInd (Name n -> Maybe (Name n)
forall a. a -> Maybe a
Just Name n
v)
          TermT n
_                                         -> MatchPlan n
forall (n :: S). MatchPlan n
MatchRec
      wantedKind = case MatchPlan n
plan of
        MatchPlan n
MatchRec   -> ElimKind
ElimRec
        MatchInd{} -> ElimKind
ElimInd
  (e, numParams) <- case
      [ er | er@(_, DataRole _ _ (DataElimKind _ _ ek)) <- elims, ek == wantedKind ] of
    (Name n
e, DataRole Name n
_ Int
numParams DataRoleKind
_) : [(Name n, DataRole n)]
_ -> (Name n, Int)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Name n, Int)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name n
e, Int
numParams)
    [] -> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Name n, Int)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TermT n -> TermT n -> TypeError n
forall (n :: S). TermT n -> TermT n -> TypeError n
TypeErrorMatchScrutineeNotData TermT n
scrut' TermT n
scrutTy)
  let dargs = case TermT n -> (TermT n, [(TypeInfo (TermT n), TermT n)])
forall (n :: S).
TermT n -> (TermT n, [(TypeInfo (TermT n), TermT n)])
collectAppSpine TermT n
scrutTy of
        (TermT n
_, [(TypeInfo (TermT n), TermT n)]
args) -> ((TypeInfo (TermT n), TermT n) -> TermT n)
-> [(TypeInfo (TermT n), TermT n)] -> [TermT n]
forall a b. (a -> b) -> [a] -> [b]
map (TypeInfo (TermT n), TermT n) -> TermT n
forall a b. (a, b) -> b
snd [(TypeInfo (TermT n), TermT n)]
args
      (paramArgs, indexArgs) = splitAt numParams dargs

  -- The bijection between branches and constructors, with per-branch arity.
  ctx <- ask
  cons <- dataConstructorsOf d
  let conIdent Name n
c = case Binder -> Maybe VarIdent
binderName (VarInfo n -> Binder
forall (n :: S). VarInfo n -> Binder
varOrig (Name n -> Context n -> VarInfo n
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name n
c Context n
ctx)) of
        Just VarIdent
x  -> VarIdent
x
        Maybe VarIdent
Nothing -> String -> VarIdent
forall a. String -> a
panicImpossible String
"a constructor entry with no name"
      conArity Name n
c = case VarInfo n -> Maybe (DataRole n)
forall (n :: S). VarInfo n -> Maybe (DataRole n)
varDataRole (Name n -> Context n -> VarInfo n
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name n
c Context n
ctx) of
        Just (DataRole Name n
_ Int
_ (DataConKind ConSort
_ Int
_ Int
numFields [Int]
recIdxs)) ->
          Int
numFields Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
recIdxs
        Maybe (DataRole n)
_ -> String -> Int
forall a. String -> a
panicImpossible String
"a constructor entry with no constructor role"
      conNames = (Name n -> VarIdent) -> [Name n] -> [VarIdent]
forall a b. (a -> b) -> [a] -> [b]
map Name n -> VarIdent
conIdent [Name n]
cons
      branchNames = ((VarIdent, Term n) -> VarIdent)
-> [(VarIdent, Term n)] -> [VarIdent]
forall a b. (a -> b) -> [a] -> [b]
map (VarIdent, Term n) -> VarIdent
forall a b. (a, b) -> a
fst [(VarIdent, Term n)]
branches
  case firstDuplicate branchNames of
    Just VarIdent
c  -> TypeError n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (VarIdent -> TypeError n
forall (n :: S). VarIdent -> TypeError n
TypeErrorMatchDuplicateBranch VarIdent
c)
    Maybe VarIdent
Nothing -> ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  case filter (`notElem` conNames) branchNames of
    VarIdent
c : [VarIdent]
_ -> TypeError n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (VarIdent -> [VarIdent] -> TypeError n
forall (n :: S). VarIdent -> [VarIdent] -> TypeError n
TypeErrorMatchUnknownBranch VarIdent
c [VarIdent]
conNames)
    []    -> ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  case filter (`notElem` branchNames) conNames of
    VarIdent
c : [VarIdent]
_ -> TypeError n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (VarIdent -> TypeError n
forall (n :: S). VarIdent -> TypeError n
TypeErrorMatchMissingBranch VarIdent
c)
    []    -> ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  let branchFor Name n
c = case VarIdent -> [(VarIdent, Term n)] -> Maybe (Term n)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Name n -> VarIdent
conIdent Name n
c) [(VarIdent, Term n)]
branches of
        Just Term n
chain -> Term n
chain
        Maybe (Term n)
Nothing    -> String -> Term n
forall a. String -> a
panicImpossible String
"a constructor without a branch after the bijection check"
  forM_ cons $ \Name n
c ->
    Bool
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Term n -> Int
forall (x :: S). Term x -> Int
armCount (Name n -> Term n
branchFor Name n
c) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Name n -> Int
conArity Name n
c) (ReaderT
   (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a b. (a -> b) -> a -> b
$
      TypeError n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError
        (VarIdent -> Int -> Int -> TypeError n
forall (n :: S). VarIdent -> Int -> Int -> TypeError n
TypeErrorMatchBranchArity (Name n -> VarIdent
conIdent Name n
c) (Name n -> Int
conArity Name n
c) (Term n -> Int
forall (x :: S). Term x -> Int
armCount (Name n -> Term n
branchFor Name n
c)))

  -- The spine: parameters, motive, methods (each branch checked against its
  -- method's Π-type), indices, scrutinee.
  atParams <- applyPlan (Var e) (map Just paramArgs)
  motive' <- case mmotive of
    Just Term n
motive -> do
      motiveTy <- TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
atParams TypeCheck n (TermT n)
-> (TermT n -> TypeCheck n (TermT n)) -> TypeCheck n (TermT n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TypeCheck n (TermT n)
-> (TermT n -> TypeCheck n (TermT n)) -> TypeCheck n (TermT n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        TypeFunT TypeInfo (TermT n)
_ Binder
_ TModality
_ TermT n
mty Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_ ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
_ -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
mty
        TermT n
_ -> String -> TypeCheck n (TermT n)
forall a. String -> a
panicImpossible String
"an eliminator's type has no motive parameter"
      typecheck motive motiveTy
    Maybe (Term n)
Nothing -> case Maybe (TermT n)
mgoal of
      Maybe (TermT n)
Nothing -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (Term n -> TypeError n
forall (n :: S). Term n -> TypeError n
TypeErrorMatchCannotInfer Term n
term)
      Just TermT n
goal -> do
        motiveTy <- TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
atParams TypeCheck n (TermT n)
-> (TermT n -> TypeCheck n (TermT n)) -> TypeCheck n (TermT n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TypeCheck n (TermT n)
-> (TermT n -> TypeCheck n (TermT n)) -> TypeCheck n (TermT n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          TypeFunT TypeInfo (TermT n)
_ Binder
_ TModality
_ TermT n
mty Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_ ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
_ -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
mty
          TermT n
_ -> String -> TypeCheck n (TermT n)
forall a. String -> a
panicImpossible String
"an eliminator's type has no motive parameter"
        scope <- asks ctxScope
        -- Under @rec-D@ the motive type has no scrutinee binder, so there
        -- is nothing to substitute (and the goal does not mention the
        -- scrutinee variable anyway — that is what chose @rec-D@). The
        -- variable to abstract is the one the plan already settled on.
        let mv = case MatchPlan n
plan of
              MatchInd Maybe (Name n)
v -> Maybe (Name n)
v
              MatchPlan n
MatchRec   -> Maybe (Name n)
forall a. Maybe a
Nothing
        pure (motiveFromGoal scope motiveTy mv goal)
  atMotive <- applyPlan atParams [Just motive']
  let applyMethods TermT n
t [] = TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
t
      applyMethods TermT n
t (Name n
c : [Name n]
rest) = TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
t TypeCheck n (TermT n)
-> (TermT n -> TypeCheck n (TermT n)) -> TypeCheck n (TermT n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TypeCheck n (TermT n)
-> (TermT n -> TypeCheck n (TermT n)) -> TypeCheck n (TermT n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        TypeFunT TypeInfo (TermT n)
_ Binder
_ TModality
_ TermT n
methodTy Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_ ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret -> do
          method <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
checkMatchArms (Name n -> Term n
branchFor Name n
c) TermT n
methodTy
          retAt <- instantiate ret method
          applyMethods (appT retAt t method) rest
        TermT n
_ -> String -> TypeCheck n (TermT n)
forall a. String -> a
panicImpossible String
"an eliminator's type runs out of method parameters"
  withMethods <- applyMethods atMotive cons
  result <- applyPlan withMethods (map Just indexArgs <> [Just scrut'])

  case mgoal of
    Maybe (TermT n)
Nothing -> ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Just TermT n
goal -> do
      resultTy <- TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
result
      -- The same tolerance as the neutral case of 'typecheck': a sketch whose
      -- branches still carry holes is accepted, the recorded holes stand.
      lenient <- not <$> asks ctxHolesAreErrors
      if lenient && containsHole result
        then unifyTypes result goal resultTy `catchError` \TypeErrorInScopedContext
_ -> ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else unifyTypes result goal resultTy
  pure result

-- | Check a branch's arm chain against its method type, one arm at a time,
-- mirroring the λ rule: each arm's binder enters the context with the domain
-- of the method's Π-type, and the elaborated arm becomes the method's λ under
-- the same binder. Holes inside the branch body therefore see the branch
-- binders as ordinary hypotheses, under the user's names.
checkMatchArms :: Distinct n => Term n -> TermT n -> TypeCheck n (TermT n)
checkMatchArms :: forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
checkMatchArms (MatchArm Binder
orig ScopedTerm n
scoped) TermT n
ty = TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TermT n
ty TypeCheck n (TermT n)
-> (TermT n -> TypeCheck n (TermT n)) -> TypeCheck n (TermT n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  ty' :: TermT n
ty'@(TypeFunT TypeInfo (TermT n)
_ Binder
_orig' TModality
md' TermT n
param0 Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope' ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret) -> do
    -- an induction hypothesis's type is the motive at a field, so it carries
    -- an administrative redex too: reduce it before it enters the context
    param' <- TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
betaMotiveApps TermT n
param0
    mapM_ checkNameShadowing (binderLeaves orig)
    body' <- elaborateUnder orig md' param' Nothing scoped $ \NameBinder n l
binder Term l
bodyTerm -> do
      mtopeIn <- (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
 -> TypeCheck l (TermT l))
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse (NameBinder n l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TypeCheck l (TermT l)
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
NameBinder n l
-> ScopedAST NameBinder sig n -> TypeCheck l (AST NameBinder sig l)
openScoped NameBinder n l
binder) Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope'
      maybe id localTope mtopeIn $ do
        retIn <- openScoped binder ret
        checkMatchArms bodyTerm retIn
    return (lambdaT ty' orig (Just (LambdaParam md' param' mtope')) body')
  -- unreachable: the arity check matches the arm count to the method's arity
  TermT n
_ -> String -> TypeCheck n (TermT n)
forall a. String -> a
panicImpossible String
"a match arm beyond its method's arity"
checkMatchArms Term n
body TermT n
ty = Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
body (TermT n -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
betaMotiveApps TermT n
ty

-- | β-reduce the administrative redexes elaboration introduces: a motive built
-- as a λ-chain and applied to a constructor form is substituted through, so a
-- branch hole's goal reads as the goal at that constructor (@nat@, or the
-- substituted dependent goal) rather than as @(λ x → …) (suc k)@. This is the
-- labelled-goal restoration of the design: nothing else is unfolded — a
-- motive that is a named family stays a named application.
betaMotiveApps :: Distinct n => TermT n -> TypeCheck n (TermT n)
betaMotiveApps :: forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
betaMotiveApps TermT n
t = case TermT n
t of
  AppT TypeInfo (TermT n)
_ TermT n
f TermT n
x -> TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
betaMotiveApps TermT n
f TypeCheck n (TermT n)
-> (TermT n -> TypeCheck n (TermT n)) -> TypeCheck n (TermT n)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    LambdaT TypeInfo (TermT n)
_ Binder
_ Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
_ ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
body -> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
ScopedTermT n -> TermT n -> TypeCheck n (TermT n)
instantiate ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
body TermT n
x
    TermT n
_                  -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
t
  TermT n
_ -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
t

-- | The number of arms in a branch's chain (the binders the branch introduces).
armCount :: Term x -> Int
armCount :: forall (x :: S). Term x -> Int
armCount (MatchArm Binder
_ (ScopedAST NameBinder x l
_ AST NameBinder (AnnSig SrcPos TermSig) l
body)) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ AST NameBinder (AnnSig SrcPos TermSig) l -> Int
forall (x :: S). Term x -> Int
armCount AST NameBinder (AnnSig SrcPos TermSig) l
body
armCount Term x
_                               = Int
0

-- | The first name occurring twice, if any.
firstDuplicate :: [VarIdent] -> Maybe VarIdent
firstDuplicate :: [VarIdent] -> Maybe VarIdent
firstDuplicate []       = Maybe VarIdent
forall a. Maybe a
Nothing
firstDuplicate (VarIdent
x : [VarIdent]
xs)
  | VarIdent
x VarIdent -> [VarIdent] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VarIdent]
xs = VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
x
  | Bool
otherwise   = [VarIdent] -> Maybe VarIdent
firstDuplicate [VarIdent]
xs

-- | A motive built from the goal: λ-binders along the motive's Π-type (the
-- family's indices, then the scrutinee), whose body is the goal — with the
-- scrutinee variable replaced by the motive's own scrutinee binder, when the
-- scrutinee is a variable. A non-variable scrutinee gives a constant family.
-- (The motive types the eliminator generator builds are literal Π-chains, so
-- matching them structurally is enough; cf. 'lambdaHoleOf'.)
motiveFromGoal
  :: Distinct n
  => Foil.Scope n -> TermT n -> Maybe (Foil.Name n) -> TermT n -> TermT n
motiveFromGoal :: forall (n :: S).
Distinct n =>
Scope n -> TermT n -> Maybe (Name n) -> TermT n -> TermT n
motiveFromGoal Scope n
scope TermT n
ty Maybe (Name n)
mv TermT n
goal = case TermT n
ty of
  TypeFunT TypeInfo (TermT n)
_info Binder
_orig TModality
_md TermT n
_param Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret ->
    Scope n
-> (forall (l :: S). DExt n l => NameBinder n l -> TermT n)
-> TermT n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall (l :: S). DExt n l => NameBinder n l -> TermT n)
 -> TermT n)
-> (forall (l :: S). DExt n l => NameBinder n l -> TermT n)
-> TermT n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
b ->
      let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
b Scope n
scope
          retAt :: AST NameBinder (AnnSig TypeInfo TermSig) l
retAt = Scope l
-> Name l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
Scope l
-> Name l -> ScopedAST NameBinder sig n -> AST NameBinder sig l
openWith Scope l
scope' (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
b) ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret
          body :: AST NameBinder (AnnSig TypeInfo TermSig) l
body = case AST NameBinder (AnnSig TypeInfo TermSig) l
retAt of
            -- an index binder: the goal does not depend on it
            TypeFunT{} -> Scope l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> Maybe (Name l)
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S).
Distinct n =>
Scope n -> TermT n -> Maybe (Name n) -> TermT n -> TermT n
motiveFromGoal Scope l
scope' AST NameBinder (AnnSig TypeInfo TermSig) l
retAt (Name n -> Name l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink (Name n -> Name l) -> Maybe (Name n) -> Maybe (Name l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Name n)
mv) (TermT n -> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
goal)
            -- the scrutinee binder
            AST NameBinder (AnnSig TypeInfo TermSig) l
_ -> case Maybe (Name n)
mv of
              Just Name n
v  -> Scope l
-> Name l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S).
Distinct n =>
Scope n -> Name n -> TermT n -> TermT n -> TermT n
substituteName Scope l
scope' (Name n -> Name l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Name n
v) (Name l -> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
b)) (TermT n -> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
goal)
              Maybe (Name n)
Nothing -> TermT n -> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
goal
       in TermT n
-> Binder
-> Maybe
     (LambdaParam
        (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n
forall (n :: S).
TermT n
-> Binder
-> Maybe (LambdaParam (ScopedTermT n) (TermT n))
-> ScopedTermT n
-> TermT n
lambdaT TermT n
ty (Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing) Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
forall a. Maybe a
Nothing (NameBinder n l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder n l
b AST NameBinder (AnnSig TypeInfo TermSig) l
body)
  TermT n
_ -> TermT n
goal

-- * Inference

inferAs :: Distinct n => TermT n -> Term n -> TypeCheck n (TermT n)
inferAs :: forall (n :: S).
Distinct n =>
TermT n -> Term n -> TypeCheck n (TermT n)
inferAs TermT n
expectedKind Term n
term = do
  term' <- Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
term
  ty <- typeOf term'
  kind <- typeOf ty
  unifyTypes ty expectedKind kind
  return term'

infer :: Distinct n => Term n -> TypeCheck n (TermT n)
infer :: forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
tt = Action n -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) a.
Distinct n =>
Action n -> TypeCheck n a -> TypeCheck n a
performing (Term n -> Action n
forall (n :: S). Term n -> Action n
ActionInfer Term n
tt) (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ case Term n
tt of
  Hole (Just VarIdent
name) | Just VarIdent
x <- VarIdent -> Maybe VarIdent
unmarkUnresolved VarIdent
name ->
    TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (VarIdent -> TypeError n
forall (n :: S). VarIdent -> TypeError n
TypeErrorUndefined VarIdent
x)
  Hole Maybe VarIdent
_mname -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (Term n -> TypeError n
forall (n :: S). Term n -> TypeError n
TypeErrorCannotInferHole Term n
tt)
  Var Name n
x -> do
    topLevel <- Name n -> TypeCheck n Bool
forall (n :: S). Name n -> TypeCheck n Bool
isTopLevelVar Name n
x
    unless topLevel $ do
      varMod <- modalityOfVar x
      locks <- locksOfVar x
      unless (coe varMod locks) $
        issueTypeError $ TypeErrorUnaccessibleVar x varMod locks
    pure (Var x)

  Term n
Universe     -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
universeT
  Term n
UniverseCube -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
cubeT
  Term n
UniverseTope -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
topeT

  Term n
CubeUnit      -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
cubeUnitT
  Term n
CubeUnitStar  -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
cubeUnitStarT

  Term n
Cube2 -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
cube2T
  Term n
Cube2_0 -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
cube2_0T
  Term n
Cube2_1 -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
cube2_1T

  Term n
CubeI -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
cubeIT
  Term n
CubeI_0 -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
cubeI_0T
  Term n
CubeI_1 -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
cubeI_1T
  CubeProduct Term n
l Term n
r -> do
    l' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
l TermT n
forall (n :: S). TermT n
cubeT
    r' <- typecheck r cubeT
    return (cubeProductT l' r')

  CubeFlip Term n
t -> do
    t' <- Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
t
    typeOf t' >>= \case
      CubeIT{} -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> TypeCheck n (TermT n))
-> TermT n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
cubeFlipT TermT n
forall (n :: S). TermT n
cubeIT TermT n
t'
      Cube2T{} -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> TypeCheck n (TermT n))
-> TermT n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
cubeFlipT TermT n
forall (n :: S). TermT n
cube2T TermT n
t'
      TermT n
ty -> do
        tyStr <- TermT n -> TypeCheck n String
forall (n :: S). TermT n -> TypeCheck n String
ppInContext TermT n
ty
        issueTypeError $ TypeErrorOther $
          "flip expects an interval cube (2 or 𝕀); got " <> tyStr
  CubeUnflip Term n
t -> do
    t' <- Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
t
    typeOf t' >>= \case
      TypeModalT TypeInfo (TermT n)
_ TModality
Op CubeIT{} -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> TypeCheck n (TermT n))
-> TermT n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
cubeUnflipT TermT n
forall (n :: S). TermT n
cubeIT TermT n
t'
      TypeModalT TypeInfo (TermT n)
_ TModality
Op Cube2T{} -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> TypeCheck n (TermT n))
-> TermT n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
cubeUnflipT TermT n
forall (n :: S). TermT n
cube2T TermT n
t'
      TermT n
ty -> do
        tyStr <- TermT n -> TypeCheck n String
forall (n :: S). TermT n -> TypeCheck n String
ppInContext TermT n
ty
        issueTypeError $ TypeErrorOther $
          "unflip expects an interval cube (2 or 𝕀) under _op; got " <> tyStr

  CubeSup Term n
l Term n
r -> do
    l' <- TermT n -> Term n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
TermT n -> Term n -> TypeCheck n (TermT n)
inferAs TermT n
forall (n :: S). TermT n
cubeT Term n
l
    r' <- inferAs cubeT r
    lTy <- typeOf l'
    rTy <- typeOf r'
    case (lTy, rTy) of
      (Cube2T{}, Cube2T{}) -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
cubeSupT TermT n
forall (n :: S). TermT n
cube2T TermT n
l' TermT n
r')
      (CubeIT{}, CubeIT{}) -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
cubeSupT TermT n
forall (n :: S). TermT n
cubeIT TermT n
l' TermT n
r')
      -- Mixed 2/𝕀 lands in 𝕀 (the join of a 2-point and an 𝕀-point), coercing
      -- the 2 side up via 2 <: 𝕀, as the adjacent TopeLEQ does.
      (CubeIT{}, Cube2T{}) -> do
        r'' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
r TermT n
forall (n :: S). TermT n
cubeIT
        return (cubeSupT cubeIT l' r'')
      (Cube2T{}, CubeIT{}) -> do
        l'' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
l TermT n
forall (n :: S). TermT n
cubeIT
        return (cubeSupT cubeIT l'' r')
      (TermT n, TermT n)
_ -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ String -> TermT n -> TermT n -> TypeError n
forall (n :: S). String -> TermT n -> TermT n -> TypeError n
TypeErrorNotIntervalCube String
"sup" TermT n
lTy TermT n
rTy

  CubeInf Term n
l Term n
r -> do
    l' <- TermT n -> Term n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
TermT n -> Term n -> TypeCheck n (TermT n)
inferAs TermT n
forall (n :: S). TermT n
cubeT Term n
l
    r' <- inferAs cubeT r
    lTy <- typeOf l'
    rTy <- typeOf r'
    case (lTy, rTy) of
      (Cube2T{}, Cube2T{}) -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
cubeInfT TermT n
forall (n :: S). TermT n
cube2T TermT n
l' TermT n
r')
      (CubeIT{}, CubeIT{}) -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
cubeInfT TermT n
forall (n :: S). TermT n
cubeIT TermT n
l' TermT n
r')
      -- Mixed 2/𝕀 lands in 𝕀 (the meet of a 2-point and an 𝕀-point), coercing
      -- the 2 side up via 2 <: 𝕀, as the adjacent TopeLEQ does.
      (CubeIT{}, Cube2T{}) -> do
        r'' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
r TermT n
forall (n :: S). TermT n
cubeIT
        return (cubeInfT cubeIT l' r'')
      (Cube2T{}, CubeIT{}) -> do
        l'' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
l TermT n
forall (n :: S). TermT n
cubeIT
        return (cubeInfT cubeIT l'' r')
      (TermT n, TermT n)
_ -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ String -> TermT n -> TermT n -> TypeError n
forall (n :: S). String -> TermT n -> TermT n -> TypeError n
TypeErrorNotIntervalCube String
"inf" TermT n
lTy TermT n
rTy

  Pair Term n
l Term n
r -> do
    l' <- Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
l
    r' <- infer r
    lt <- typeOf l'
    rt <- typeOf r'
    typeOf lt >>= \case
      --    Γ ⊢ l ⇒ (I : CUBE)
      --    Γ ⊢ r ⇒ (J : CUBE)
      -- ———————————————————————————
      -- Γ ⊢ (l, r) ⇒ (I × J : CUBE)
      UniverseCubeT{} -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
pairT (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
cubeProductT TermT n
lt TermT n
rt) TermT n
l' TermT n
r')
      --    Γ ⊢ l ⇒ (A : U)
      --    Γ ⊢ r ⇒ (B : U)
      -- ———————————————————————————
      -- Γ ⊢ (l, r) ⇒ (A × B : U)             where A × B = Σ (_ : A), B
      TermT n
_ -> do
        -- NOTE: infer as a non-dependent pair!
        rtScope <- TermT n -> TypeCheck n (ScopedTermT n)
forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n (ScopedTermT n)
constScope TermT n
rt
        return (pairT (typeSigmaT (BinderVar Nothing) Id lt rtScope) l' r')

  First Term n
t -> do
    t' <- Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
t
    fmap stripTypeRestrictions (typeOf t') >>= \case
      RecBottomT{} -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
recBottomT -- FIXME: is this ok?
      TypeSigmaT TypeInfo (TermT n)
_ty Binder
_orig TModality
_md TermT n
lt ScopedTermT n
_rt ->
        TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT TermT n
lt TermT n
t')
      CubeProductT TypeInfo (TermT n)
_ty TermT n
l TermT n
_r ->
        TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT TermT n
l TermT n
t')
      TermT n
ty -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ TermT n -> TermT n -> TypeError n
forall (n :: S). TermT n -> TermT n -> TypeError n
TypeErrorNotPair TermT n
t' TermT n
ty

  Second Term n
t -> do
    t' <- Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
t
    fmap stripTypeRestrictions (typeOf t') >>= \case
      RecBottomT{} -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
recBottomT -- FIXME: is this ok?
      TypeSigmaT TypeInfo (TermT n)
_ty Binder
_orig TModality
_md TermT n
lt ScopedTermT n
rt -> do
        rtAt <- ScopedTermT n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
ScopedTermT n -> TermT n -> TypeCheck n (TermT n)
instantiate ScopedTermT n
rt (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT TermT n
lt TermT n
t')
        return (secondT rtAt t')
      CubeProductT TypeInfo (TermT n)
_ty TermT n
_l TermT n
r ->
        TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
secondT TermT n
r TermT n
t')
      TermT n
ty -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ TermT n -> TermT n -> TypeError n
forall (n :: S). TermT n -> TermT n -> TypeError n
TypeErrorNotPair TermT n
t' TermT n
ty

  Term n
TypeUnit -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
typeUnitT
  Term n
Unit -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
unitT

  Term n
TopeTop -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
topeTopT
  Term n
TopeBottom -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
forall (n :: S). TermT n
topeBottomT

  TopeEQ Term n
l Term n
r -> do
    l' <- TermT n -> Term n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
TermT n -> Term n -> TypeCheck n (TermT n)
inferAs TermT n
forall (n :: S). TermT n
cubeT Term n
l
    lt <- typeOf l'
    r' <- typecheck r lt
    return (topeEQT l' r')

  TopeLEQ Term n
l Term n
r -> do
    l' <- TermT n -> Term n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
TermT n -> Term n -> TypeCheck n (TermT n)
inferAs TermT n
forall (n :: S). TermT n
cubeT Term n
l
    r' <- inferAs cubeT r
    lTy <- typeOf l'
    rTy <- typeOf r'
    case (lTy, rTy) of
      (Cube2T{}, Cube2T{}) -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
l' TermT n
r')
      (CubeIT{}, CubeIT{}) -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
l' TermT n
r')
      (CubeIT{}, Cube2T{}) -> do
        r'' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
r TermT n
forall (n :: S). TermT n
cubeIT
        return (topeLEQT l' r'')
      (Cube2T{}, CubeIT{}) -> do
        l'' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
l TermT n
forall (n :: S). TermT n
cubeIT
        return (topeLEQT l'' r')
      (TermT n, TermT n)
_ -> do
        lStr <- TermT n -> TypeCheck n String
forall (n :: S). TermT n -> TypeCheck n String
ppInContext TermT n
lTy
        rStr <- ppInContext rTy
        issueTypeError $ TypeErrorOther $
          "the (t ≤ s) tope expects points in interval cubes (2 or 𝕀); got "
            <> lStr <> " and " <> rStr

  TopeAnd Term n
l Term n
r -> do
    l' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
l TermT n
forall (n :: S). TermT n
topeT
    r' <- typecheck r topeT
    return (topeAndT l' r')

  TopeOr Term n
l Term n
r -> do
    l' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
l TermT n
forall (n :: S). TermT n
topeT
    r' <- typecheck r topeT
    return (topeOrT l' r')

  TopeInv Term n
t -> do
    t' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
t TermT n
forall (n :: S). TermT n
topeT
    return (topeInvT t')

  TopeUninv Term n
t -> do
    t' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
t (TermT n -> TModality -> TermT n -> TermT n
forall (n :: S). TermT n -> TModality -> TermT n -> TermT n
typeModalT TermT n
forall (n :: S). TermT n
universeT TModality
Op TermT n
forall (n :: S). TermT n
topeT)
    return (topeUninvT t')

  Term n
RecBottom -> do
    TermT n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S). Distinct n => TermT n -> TypeCheck n ()
contextEntails TermT n
forall (n :: S). TermT n
topeBottomT
    TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return TermT n
forall (n :: S). TermT n
recBottomT

  RecOr [(Term n, Term n)]
rs -> do
    ttts <- [(Term n, Term n)]
-> ((Term n, Term n)
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (TermT n, (TermT n, TermT n)))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(TermT n, (TermT n, TermT n))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Term n, Term n)]
rs (((Term n, Term n)
  -> ReaderT
       (Context n)
       (ExceptT TypeErrorInScopedContext (State CheckLog))
       (TermT n, (TermT n, TermT n)))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [(TermT n, (TermT n, TermT n))])
-> ((Term n, Term n)
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (TermT n, (TermT n, TermT n)))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(TermT n, (TermT n, TermT n))]
forall a b. (a -> b) -> a -> b
$ \(Term n
tope, Term n
term) -> do
      tope' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
tope TermT n
forall (n :: S). TermT n
topeT
      -- NOTE: branch guards need not be contained in the context. recOR requires
      -- only coverage (context |- OR(guards)); a guard may overhang the context (when
      -- splitting with a named shape, say). checkTopeAgainstContext warns on overhang
      -- and errors only if the guard is disjoint from the context (a vacuous branch).
      checkTopeAgainstContext "recOR branch guard" tope'
      localTope tope' $ do
        term' <- inferAs universeT term
        ty <- typeOf term'
        return (tope', (term', ty))
    let rs' = ((TermT n, (TermT n, TermT n)) -> (TermT n, TermT n))
-> [(TermT n, (TermT n, TermT n))] -> [(TermT n, TermT n)]
forall a b. (a -> b) -> [a] -> [b]
map (((TermT n, TermT n) -> TermT n)
-> (TermT n, (TermT n, TermT n)) -> (TermT n, TermT n)
forall a b. (a -> b) -> (TermT n, a) -> (TermT n, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TermT n, TermT n) -> TermT n
forall a b. (a, b) -> a
fst) [(TermT n, (TermT n, TermT n))]
ttts
        ts  = ((TermT n, (TermT n, TermT n)) -> (TermT n, TermT n))
-> [(TermT n, (TermT n, TermT n))] -> [(TermT n, TermT n)]
forall a b. (a -> b) -> [a] -> [b]
map (((TermT n, TermT n) -> TermT n)
-> (TermT n, (TermT n, TermT n)) -> (TermT n, TermT n)
forall a b. (a -> b) -> (TermT n, a) -> (TermT n, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TermT n, TermT n) -> TermT n
forall a b. (a, b) -> b
snd) [(TermT n, (TermT n, TermT n))]
ttts
    sequence_ [ checkCoherence l r | l:rs'' <- tails rs', r <- rs'' ]
    contextEntailsUnion (map fst ttts)
    return (recOrT (recOrT universeT ts) rs')

  TypeFun Binder
orig TModality
md Term n
a Maybe (ScopedTerm n)
Nothing ScopedTerm n
b -> do
    a' <- TModality -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
md (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
a
    typeOf a' >>= \case
      -- an argument can be a type
      UniverseT{} ->
        case TermT n
a' of
          -- except if it is the TOPE universe
          UniverseTopeT{} ->
            TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ String -> TypeError n
forall (n :: S). String -> TypeError n
TypeErrorOther String
"tope params are illegal"
          TermT n
_ -> do
            (VarIdent
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> [VarIdent]
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VarIdent
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S). VarIdent -> TypeCheck n ()
checkNameShadowing (Binder -> [VarIdent]
binderLeaves Binder
orig)
            b' <- Binder
-> TModality
-> TermT n
-> Maybe (TermT n)
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l (TermT l))
-> TypeCheck n (ScopedTermT n)
forall (n :: S).
Distinct n =>
Binder
-> TModality
-> TermT n
-> Maybe (TermT n)
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l (TermT l))
-> TypeCheck n (ScopedTermT n)
elaborateUnder Binder
orig TModality
md TermT n
a' Maybe (TermT n)
forall a. Maybe a
Nothing ScopedTerm n
b ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> Term l -> TypeCheck l (TermT l))
 -> TypeCheck n (ScopedTermT n))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l (TermT l))
-> TypeCheck n (ScopedTermT n)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
_binder Term l
bTerm ->
              Term l -> TermT l -> TypeCheck l (TermT l)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term l
bTerm TermT l
forall (n :: S). TermT n
universeT
            return (typeFunT orig md a' Nothing b')
      -- an argument can be a cube
      UniverseCubeT{} -> do
        (VarIdent
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> [VarIdent]
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VarIdent
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S). VarIdent -> TypeCheck n ()
checkNameShadowing (Binder -> [VarIdent]
binderLeaves Binder
orig)
        b' <- Binder
-> TModality
-> TermT n
-> Maybe (TermT n)
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l (TermT l))
-> TypeCheck n (ScopedTermT n)
forall (n :: S).
Distinct n =>
Binder
-> TModality
-> TermT n
-> Maybe (TermT n)
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l (TermT l))
-> TypeCheck n (ScopedTermT n)
elaborateUnder Binder
orig TModality
md TermT n
a' Maybe (TermT n)
forall a. Maybe a
Nothing ScopedTerm n
b ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> Term l -> TypeCheck l (TermT l))
 -> TypeCheck n (ScopedTermT n))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l (TermT l))
-> TypeCheck n (ScopedTermT n)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
_binder Term l
bTerm ->
          Term l -> TermT l -> TypeCheck l (TermT l)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term l
bTerm TermT l
forall (n :: S). TermT n
universeT
        return (typeFunT orig md a' Nothing b')
      -- an argument can be a shape
      TypeFunT TypeInfo (TermT n)
_ty Binder
_orig TModality
_md TermT n
cube Maybe (ScopedTermT n)
mtope (ScopedAST NameBinder n l
_ UniverseTopeT{}) -> do
        (VarIdent
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> [VarIdent]
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VarIdent
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S). VarIdent -> TypeCheck n ()
checkNameShadowing (Binder -> [VarIdent]
binderLeaves Binder
orig)
        (tope', b') <- Binder
-> TModality
-> TermT n
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l
    -> Term l -> TypeCheck l (ScopedTermT n, ScopedTermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (ScopedTermT n, ScopedTermT n)
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l a)
-> TypeCheck n a
checkUnder Binder
orig TModality
md TermT n
cube ScopedTerm n
b ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l
  -> Term l -> TypeCheck l (ScopedTermT n, ScopedTermT n))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (ScopedTermT n, ScopedTermT n))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l
    -> Term l -> TypeCheck l (ScopedTermT n, ScopedTermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (ScopedTermT n, ScopedTermT n)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder Term l
bTerm -> do
          -- eta expand a' into a tope over the bound variable
          let etaTope :: TermT l
etaTope = TermT l -> TermT l -> TermT l -> TermT l
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT TermT l
forall (n :: S). TermT n
topeT (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
a') (Name l -> TermT l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder))
          tope' <- case Maybe (ScopedTermT n)
mtope of
            Maybe (ScopedTermT n)
Nothing     -> TermT l
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT l)
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT l
etaTope
            Just ScopedTermT n
tope'' -> do
              inner <- NameBinder n l
-> ScopedTermT n
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT l)
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
NameBinder n l
-> ScopedAST NameBinder sig n -> TypeCheck l (AST NameBinder sig l)
openScoped NameBinder n l
binder ScopedTermT n
tope''
              pure (topeAndT inner etaTope)
          bTyped <- localTope etaTope $ typecheck bTerm universeT
          pure (ScopedAST binder tope', ScopedAST binder bTyped)
        return (typeFunT orig md cube (Just tope') b')
      TermT n
ty -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TermT n -> TypeError n
forall (n :: S). Term n -> TermT n -> TypeError n
TypeErrorInvalidArgumentType Term n
a TermT n
ty

  TypeFun Binder
orig TModality
md Term n
cube (Just ScopedTerm n
tope) ScopedTerm n
ret -> do
    cube' <- TModality -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
md (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
cube TermT n
forall (n :: S). TermT n
cubeT
    mapM_ checkNameShadowing (binderLeaves orig)
    (tope', ret') <- checkUnder orig md cube' tope $ \NameBinder n l
binder Term l
topeTerm -> do
      topeTyped <- Term l -> TermT l -> TypeCheck l (TermT l)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term l
topeTerm TermT l
forall (n :: S). TermT n
topeT
      retTerm <- openScoped binder ret
      retTyped <- localTope topeTyped $ typecheck retTerm universeT
      pure (ScopedAST binder topeTyped, ScopedAST binder retTyped)
    return (typeFunT orig md cube' (Just tope') ret')

  TypeSigma Binder
orig TModality
md Term n
a ScopedTerm n
b -> do
    a' <- TModality -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
md (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
a TermT n
forall (n :: S). TermT n
universeT
    mapM_ checkNameShadowing (binderLeaves orig)
    b' <- elaborateUnder orig md a' Nothing b $ \NameBinder n l
_binder Term l
bTerm ->
      Term l -> TermT l -> TypeCheck l (TermT l)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term l
bTerm TermT l
forall (n :: S). TermT n
universeT
    return (typeSigmaT orig md a' b')

  TypeId Term n
x (Just Term n
tA) Term n
y -> do
    tA' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
tA TermT n
forall (n :: S). TermT n
universeT
    x' <- typecheck x tA'
    y' <- typecheck y tA'
    return (typeIdT x' (Just tA') y')

  TypeId Term n
x Maybe (Term n)
Nothing Term n
y -> do
    x' <- TermT n -> Term n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
TermT n -> Term n -> TypeCheck n (TermT n)
inferAs TermT n
forall (n :: S). TermT n
universeT Term n
x
    tA <- typeOf x'
    y' <- typecheck y tA
    return (typeIdT x' (Just tA) y')

  App Term n
f Term n
x -> do
    f' <- TermT n -> Term n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
TermT n -> Term n -> TypeCheck n (TermT n)
inferAs TermT n
forall (n :: S). TermT n
universeT Term n
f
    fmap stripTypeRestrictions (typeOf f') >>= \case
      TypeFunT TypeInfo (TermT n)
_ty Binder
orig TModality
md TermT n
a Maybe (ScopedTermT n)
mtope ScopedTermT n
b -> do
        -- A hole argument to a shape-restricted function carries the shape as its
        -- goal: record (binder : a | tope) rather than just the cube a.
        x' <- TModality -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
md (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ case (Term n
x, Maybe (ScopedTermT n)
mtope) of
          (Hole Maybe VarIdent
mname, Just ScopedTermT n
tope) -> Maybe VarIdent
-> Binder -> TermT n -> ScopedTermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Maybe VarIdent
-> Binder -> TermT n -> ScopedTermT n -> TypeCheck n (TermT n)
checkHoleAgainstShape Maybe VarIdent
mname Binder
orig TermT n
a ScopedTermT n
tope
          (Term n, Maybe (ScopedTermT n))
_                       -> Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
x TermT n
a
        bAt <- instantiate b x'
        let result = TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT TermT n
bAt TermT n
f' TermT n
x'
        case b of
          ScopedAST NameBinder n l
_ UniverseTopeT{} ->
            case Maybe (ScopedTermT n)
mtope of
              Maybe (ScopedTermT n)
Nothing -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return TermT n
result
              Just ScopedTermT n
tope -> do
                topeAt <- ScopedTermT n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
ScopedTermT n -> TermT n -> TypeCheck n (TermT n)
instantiate ScopedTermT n
tope TermT n
x'
                return (topeAndT topeAt result)
          ScopedTermT n
_ -> do
            -- FIXME: need to check?
            Maybe (ScopedTermT n)
-> (ScopedTermT n
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Maybe (ScopedTermT n)
mtope ((ScopedTermT n
  -> ReaderT
       (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> (ScopedTermT n
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a b. (a -> b) -> a -> b
$ \ScopedTermT n
tope -> do
              topeAt <- ScopedTermT n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
ScopedTermT n -> TermT n -> TypeCheck n (TermT n)
instantiate ScopedTermT n
tope TermT n
x'
              contextEntails topeAt
            TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return TermT n
result
      TermT n
ty -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ TermT n -> TermT n -> TypeError n
forall (n :: S). TermT n -> TermT n -> TypeError n
TypeErrorNotFunction TermT n
f' TermT n
ty

  Lambda Binder
_orig Maybe (LambdaParam (ScopedTerm n) (Term n))
Nothing ScopedTerm n
_body ->
    TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TypeError n
forall (n :: S). Term n -> TypeError n
TypeErrorCannotInferBareLambda Term n
tt

  Lambda Binder
orig (Just (LambdaParam TModality
md Term n
ty Maybe (ScopedTerm n)
Nothing)) ScopedTerm n
body -> do
    ty' <- TModality -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
md (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
ty
    mcube <- typeOf ty' >>= \case
      -- an argument can be a type
      UniverseT{} ->
        case TermT n
ty' of
          -- except if it is the TOPE universe
          UniverseTopeT{} ->
            TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe (TermT n)))
-> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a b. (a -> b) -> a -> b
$ String -> TypeError n
forall (n :: S). String -> TypeError n
TypeErrorOther String
"tope params are illegal"
          TermT n
_ -> Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (TermT n)
forall a. Maybe a
Nothing
      -- an argument can be a cube
      UniverseCubeT{} -> Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (TermT n)
forall a. Maybe a
Nothing
      -- an argument can be a shape
      TypeFunT TypeInfo (TermT n)
_ty Binder
_orig TModality
_md TermT n
cube Maybe (ScopedTermT n)
_mtope (ScopedAST NameBinder n l
_ UniverseTopeT{}) -> do
        (VarIdent
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> [VarIdent]
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VarIdent
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S). VarIdent -> TypeCheck n ()
checkNameShadowing (Binder -> [VarIdent]
binderLeaves Binder
orig)
        Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
cube)
      TermT n
kind -> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe (TermT n)))
-> TypeError n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a b. (a -> b) -> a -> b
$ Term n -> TermT n -> TypeError n
forall (n :: S). Term n -> TermT n -> TypeError n
TypeErrorInvalidArgumentType Term n
ty TermT n
kind
    mapM_ checkNameShadowing (binderLeaves orig)
    let param = TermT n -> Maybe (TermT n) -> TermT n
forall a. a -> Maybe a -> a
fromMaybe TermT n
ty' Maybe (TermT n)
mcube
    case mcube of
      Maybe (TermT n)
Nothing -> do
        (body', ret) <- Binder
-> TModality
-> TermT n
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l
    -> Term l -> TypeCheck l (ScopedTermT n, ScopedTermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (ScopedTermT n, ScopedTermT n)
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l a)
-> TypeCheck n a
checkUnder Binder
orig TModality
md TermT n
param ScopedTerm n
body ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l
  -> Term l -> TypeCheck l (ScopedTermT n, ScopedTermT n))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (ScopedTermT n, ScopedTermT n))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l
    -> Term l -> TypeCheck l (ScopedTermT n, ScopedTermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (ScopedTermT n, ScopedTermT n)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder Term l
bodyTerm -> do
          body' <- Term l -> TypeCheck l (TermT l)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term l
bodyTerm
          ret <- typeOf body'
          pure (ScopedAST binder body', ScopedAST binder ret)
        return (lambdaT (typeFunT orig md param Nothing ret) orig
                  (Just (LambdaParam md param Nothing)) body')
      Just TermT n
_ -> do
        (tope', body', ret) <- Binder
-> TModality
-> TermT n
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l
    -> Term l
    -> TypeCheck l (ScopedTermT n, ScopedTermT n, ScopedTermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (ScopedTermT n, ScopedTermT n, ScopedTermT n)
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l a)
-> TypeCheck n a
checkUnder Binder
orig TModality
md TermT n
param ScopedTerm n
body ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l
  -> Term l
  -> TypeCheck l (ScopedTermT n, ScopedTermT n, ScopedTermT n))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (ScopedTermT n, ScopedTermT n, ScopedTermT n))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l
    -> Term l
    -> TypeCheck l (ScopedTermT n, ScopedTermT n, ScopedTermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (ScopedTermT n, ScopedTermT n, ScopedTermT n)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder Term l
bodyTerm -> do
          -- eta expand the shape into a tope over the bound variable
          let etaTope :: TermT l
etaTope = TermT l -> TermT l -> TermT l -> TermT l
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT TermT l
forall (n :: S). TermT n
topeT (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
ty') (Name l -> TermT l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder))
          body' <- TermT l -> TypeCheck l (TermT l) -> TypeCheck l (TermT l)
forall (n :: S) a.
Distinct n =>
TermT n -> TypeCheck n a -> TypeCheck n a
localTope TermT l
etaTope (TypeCheck l (TermT l) -> TypeCheck l (TermT l))
-> TypeCheck l (TermT l) -> TypeCheck l (TermT l)
forall a b. (a -> b) -> a -> b
$ Term l -> TypeCheck l (TermT l)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term l
bodyTerm
          ret <- typeOf body'
          pure (ScopedAST binder etaTope, ScopedAST binder body', ScopedAST binder ret)
        return (lambdaT (typeFunT orig md param (Just tope') ret) orig
                  (Just (LambdaParam md param (Just tope'))) body')

  Lambda Binder
orig (Just (LambdaParam TModality
md Term n
cube (Just ScopedTerm n
tope))) ScopedTerm n
body -> do
    cube' <- TModality -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
md (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
cube TermT n
forall (n :: S). TermT n
cubeT
    mapM_ checkNameShadowing (binderLeaves orig)
    (tope', body', ret) <- checkUnder orig md cube' tope $ \NameBinder n l
binder Term l
topeTerm -> do
      topeTyped <- Term l -> TypeCheck l (TermT l)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term l
topeTerm
      bodyTerm <- openScoped binder body
      body' <- localTope topeTyped $ infer bodyTerm
      ret <- typeOf body'
      pure (ScopedAST binder topeTyped, ScopedAST binder body', ScopedAST binder ret)
    return (lambdaT (typeFunT orig md cube' (Just tope') ret) orig
              (Just (LambdaParam md cube' (Just tope'))) body')

  Let Binder
orig Maybe (Term n)
annot Term n
val ScopedTerm n
body -> do
    val' <- Action n -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) a.
Distinct n =>
Action n -> TypeCheck n a -> TypeCheck n a
performing (Maybe VarIdent -> Action n
forall (n :: S). Maybe VarIdent -> Action n
ActionCheckLetValue (Binder -> Maybe VarIdent
binderName Binder
orig)) (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ case Maybe (Term n)
annot of
      Maybe (Term n)
Nothing -> Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
val
      Just Term n
ty -> do
        bindTy <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
ty TermT n
forall (n :: S). TermT n
universeT
        typecheck val bindTy
    bindTy <- typeOf val'
    (body', ret) <- checkUnderWith orig Id bindTy (Just val') body $ \NameBinder n l
binder Term l
bodyTerm -> do
      body' <- Term l -> TypeCheck l (TermT l)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term l
bodyTerm
      ret <- typeOf body'
      pure (ScopedAST binder body', ScopedAST binder ret)
    retAt <- instantiate ret val'
    return (letT retAt orig (Just bindTy) val' body')

  LetMod Binder
orig TModality
app TModality
inn Maybe (Term n)
annot Maybe (Term n)
mmotive Term n
val ScopedTerm n
body -> do
    val' <- Action n -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) a.
Distinct n =>
Action n -> TypeCheck n a -> TypeCheck n a
performing (Maybe VarIdent -> Action n
forall (n :: S). Maybe VarIdent -> Action n
ActionCheckLetValue (Binder -> Maybe VarIdent
binderName Binder
orig)) (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ case Maybe (Term n)
annot of
      Maybe (Term n)
Nothing -> TModality -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
app (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
val
      Just Term n
bindType -> do
        bindType' <- Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
bindType
        bindUniv <- typeOf bindType'
        enterModality app $ typecheck val (typeModalT bindUniv inn bindType')
    valTy <- typeOf val'
    bindTy <- case valTy of
      TypeModalT TypeInfo (TermT n)
_ty TModality
md TermT n
t | TModality
md TModality -> TModality -> Bool
forall a. Eq a => a -> a -> Bool
== TModality
inn -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return TermT n
t
      TermT n
o -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TModality -> TermT n -> TypeError n
forall (n :: S). Term n -> TModality -> TermT n -> TypeError n
TypeErrorNotModal (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
o) TModality
inn TermT n
val'
    bindVal <- whnfT val' >>= \case
      ModAppT TypeInfo (TermT n)
_ty TModality
_m TermT n
t -> Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
t)
      TermT n
o | TModality -> Bool
forall m. ModeTheory m => m -> Bool
isRA TModality
inn -> Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just (TermT n -> TModality -> TModality -> TermT n -> TermT n
forall (n :: S).
TermT n -> TModality -> TModality -> TermT n -> TermT n
modExtractT TermT n
bindTy TModality
app TModality
inn TermT n
o))
      TermT n
_ -> Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (TermT n)
forall a. Maybe a
Nothing
    -- The motive is a family over the modal value, @(z :^app ⟨inn|A⟩) → U@, so its
    -- binder stands for the whole @val@ and not for the let-bound @orig : A@; it is
    -- left anonymous rather than reusing @orig@, which would show the wrong role in
    -- goals and hovers. Only @U@ is supported as the codomain for now: a motive
    -- landing in @CUBE@ or @TOPE@ cannot be written.
    univScope <- constScope universeT
    mmotive' <- forM mmotive $ \Term n
motive ->
      Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
motive (Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
forall (n :: S).
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
typeFunT (Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing) TModality
app TermT n
valTy Maybe (ScopedTermT n)
forall a. Maybe a
Nothing ScopedTermT n
univScope)
    case mmotive' of
      Just TermT n
motive' -> do
        body' <- Binder
-> TModality
-> TermT n
-> Maybe (TermT n)
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l (TermT l))
-> TypeCheck n (ScopedTermT n)
forall (n :: S).
Distinct n =>
Binder
-> TModality
-> TermT n
-> Maybe (TermT n)
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l (TermT l))
-> TypeCheck n (ScopedTermT n)
elaborateUnder Binder
orig (TModality -> TModality -> TModality
forall m. ModeTheory m => m -> m -> m
comp TModality
app TModality
inn) TermT n
bindTy Maybe (TermT n)
bindVal ScopedTerm n
body ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> Term l -> TypeCheck l (TermT l))
 -> TypeCheck n (ScopedTermT n))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l (TermT l))
-> TypeCheck n (ScopedTermT n)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder Term l
bodyTerm ->
          Term l -> TermT l -> TypeCheck l (TermT l)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term l
bodyTerm
            (TermT l -> TermT l -> TermT l -> TermT l
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT TermT l
forall (n :: S). TermT n
universeT (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
motive')
              (TermT l -> TModality -> TermT l -> TermT l
forall (n :: S). TermT n -> TModality -> TermT n -> TermT n
modAppT (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
valTy) TModality
inn (Name l -> TermT l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder))))
        return (letModT (appT universeT motive' val') orig app inn (Just bindTy) mmotive' val' body')
      Maybe (TermT n)
Nothing -> do
        (body', ret) <- Binder
-> TModality
-> TermT n
-> Maybe (TermT n)
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l
    -> Term l -> TypeCheck l (ScopedTermT n, ScopedTermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (ScopedTermT n, ScopedTermT n)
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> Maybe (TermT n)
-> ScopedTerm n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> Term l -> TypeCheck l a)
-> TypeCheck n a
checkUnderWith Binder
orig (TModality -> TModality -> TModality
forall m. ModeTheory m => m -> m -> m
comp TModality
app TModality
inn) TermT n
bindTy Maybe (TermT n)
bindVal ScopedTerm n
body ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l
  -> Term l -> TypeCheck l (ScopedTermT n, ScopedTermT n))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (ScopedTermT n, ScopedTermT n))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l
    -> Term l -> TypeCheck l (ScopedTermT n, ScopedTermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (ScopedTermT n, ScopedTermT n)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder Term l
bodyTerm -> do
          body' <- Term l -> TypeCheck l (TermT l)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term l
bodyTerm
          ret <- typeOf body'
          pure (ScopedAST binder body', ScopedAST binder ret)
        retAt <- instantiate ret val'
        return (letModT retAt orig app inn (Just bindTy) Nothing val' body')

  Refl Maybe (Term n, Maybe (Term n))
Nothing -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TypeError n
forall (n :: S). Term n -> TypeError n
TypeErrorCannotInferBareRefl Term n
tt
  Refl (Just (Term n
x, Maybe (Term n)
Nothing)) -> do
    x' <- TermT n -> Term n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
TermT n -> Term n -> TypeCheck n (TermT n)
inferAs TermT n
forall (n :: S). TermT n
universeT Term n
x
    ty <- typeOf x'
    return (reflT (typeIdT x' (Just ty) x') (Just (x', Just ty)))
  Refl (Just (Term n
x, Just Term n
ty)) -> do
    ty' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
ty TermT n
forall (n :: S). TermT n
universeT
    x' <- typecheck x ty'
    return (reflT (typeIdT x' (Just ty') x') (Just (x', Just ty')))

  IdJ Term n
tA Term n
a Term n
tC Term n
d Term n
x Term n
p -> do
    tA' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
tA TermT n
forall (n :: S). TermT n
universeT
    a' <- typecheck a tA'
    typeOf_C <- motiveType tA' a'
    tC' <- typecheck tC typeOf_C
    univScope <- constScope universeT
    let typeOf_d =
          TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT TermT n
forall (n :: S). TermT n
universeT
            (TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT (Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
forall (n :: S).
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
typeFunT (Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing) TModality
Id (TermT n -> Maybe (TermT n) -> TermT n -> TermT n
forall (n :: S). TermT n -> Maybe (TermT n) -> TermT n -> TermT n
typeIdT TermT n
a' (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
tA') TermT n
a') Maybe (ScopedTermT n)
forall a. Maybe a
Nothing ScopedTermT n
univScope)
              TermT n
tC' TermT n
a')
            (TermT n -> Maybe (TermT n, Maybe (TermT n)) -> TermT n
forall (n :: S).
TermT n -> Maybe (TermT n, Maybe (TermT n)) -> TermT n
reflT (TermT n -> Maybe (TermT n) -> TermT n -> TermT n
forall (n :: S). TermT n -> Maybe (TermT n) -> TermT n -> TermT n
typeIdT TermT n
a' (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
tA') TermT n
a') Maybe (TermT n, Maybe (TermT n))
forall a. Maybe a
Nothing)
    d' <- typecheck d typeOf_d
    x' <- typecheck x tA'
    p' <- typecheck p (typeIdT a' (Just tA') x')
    let ret =
          TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT TermT n
forall (n :: S). TermT n
universeT
            (TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT (Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
forall (n :: S).
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
typeFunT (Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing) TModality
Id (TermT n -> Maybe (TermT n) -> TermT n -> TermT n
forall (n :: S). TermT n -> Maybe (TermT n) -> TermT n -> TermT n
typeIdT TermT n
a' (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
tA') TermT n
x') Maybe (ScopedTermT n)
forall a. Maybe a
Nothing ScopedTermT n
univScope)
              TermT n
tC' TermT n
x')
            TermT n
p'
    return (idJT ret tA' a' tC' d' x' p')

  TypeAsc Term n
term Term n
ty -> do
    ty' <- TermT n -> Term n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
TermT n -> Term n -> TypeCheck n (TermT n)
inferAs TermT n
forall (n :: S). TermT n
universeT Term n
ty -- this works on types AND cubes
    term' <- typecheck term ty'
    return (typeAscT term' ty')

  TypeRestricted Term n
ty [(Term n, Term n)]
rs -> do
    ty' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
ty TermT n
forall (n :: S). TermT n
universeT
    rs' <- forM rs $ \(Term n
tope, Term n
term) -> do
      tope' <- Term n -> TermT n -> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n -> TermT n -> TypeCheck n (TermT n)
typecheck Term n
tope TermT n
forall (n :: S). TermT n
topeT
      term' <- localTope tope' $ typecheck term ty'
      return (tope', term')
    sequence_ [ checkCoherence l r | l:rs'' <- tails rs', r <- rs'' ]
    return (typeRestrictedT ty' rs')

  TypeModal TModality
md Term n
ty -> do
    ty' <- TModality -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
md (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
ty
    universeTy <- typeOf ty'
    _ <- case universeTy of
      UniverseT{}     -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
universeTy
      UniverseCubeT{} -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
universeTy
      UniverseTopeT{} -> TermT n -> TypeCheck n (TermT n)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TermT n
universeTy
      TermT n
_               -> TypeError n -> TypeCheck n (TermT n)
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TypeError n -> TypeCheck n (TermT n))
-> TypeError n -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ TermT n -> TypeError n
forall (n :: S). TermT n -> TypeError n
TypeErrorNotTypeInModal TermT n
universeTy
    return (typeModalT universeTy md ty')

  ModApp TModality
md Term n
term -> do
    term' <- TModality -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
md (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ Term n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => Term n -> TypeCheck n (TermT n)
infer Term n
term
    ty <- typeOf term'
    tyUniv <- typeOf ty
    return $ modAppT (typeModalT tyUniv md ty) md term'

  ModExtract{} -> String -> TypeCheck n (TermT n)
forall a. String -> a
panicImpossible String
"extract is an internal term and cannot be inferred"

  -- A match infers only through its "into" motive; 'checkMatch' rejects it
  -- otherwise, since there is no goal to build the motive from.
  Match Term n
scrut Maybe (Term n)
mmotive [(VarIdent, Term n)]
branches -> Term n
-> Term n
-> Maybe (Term n)
-> [(VarIdent, Term n)]
-> Maybe (TermT n)
-> TypeCheck n (TermT n)
forall (n :: S).
Distinct n =>
Term n
-> Term n
-> Maybe (Term n)
-> [(VarIdent, Term n)]
-> Maybe (TermT n)
-> TypeCheck n (TermT n)
checkMatch Term n
tt Term n
scrut Maybe (Term n)
mmotive [(VarIdent, Term n)]
branches Maybe (TermT n)
forall a. Maybe a
Nothing
  MatchArm{} -> String -> TypeCheck n (TermT n)
forall a. String -> a
panicImpossible String
"a match arm outside of a match branch"

-- | The type of the motive of a path induction: @(z : A) → (a =_A z) → U@.
motiveType :: Distinct n => TermT n -> TermT n -> TypeCheck n (TermT n)
motiveType :: forall (n :: S).
Distinct n =>
TermT n -> TermT n -> TypeCheck n (TermT n)
motiveType TermT n
tA TermT n
a = do
  scope <- (Context n -> Scope n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Scope n)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context n -> Scope n
forall (n :: S). Context n -> Scope n
ctxScope
  pure $ Foil.withFresh scope $ \NameBinder n l
zBinder ->
    let scopeZ :: Scope l
scopeZ = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
zBinder Scope n
scope
        idType :: TermT l
idType = TermT l -> Maybe (TermT l) -> TermT l -> TermT l
forall (n :: S). TermT n -> Maybe (TermT n) -> TermT n -> TermT n
typeIdT (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
a) (TermT l -> Maybe (TermT l)
forall a. a -> Maybe a
Just (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
tA)) (Name l -> TermT l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
zBinder))
     in Scope l
-> (forall (l :: S). DExt l l => NameBinder l l -> TermT n)
-> TermT n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope l
scopeZ ((forall (l :: S). DExt l l => NameBinder l l -> TermT n)
 -> TermT n)
-> (forall (l :: S). DExt l l => NameBinder l l -> TermT n)
-> TermT n
forall a b. (a -> b) -> a -> b
$ \NameBinder l l
pBinder ->
          Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
forall (n :: S).
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
typeFunT (Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing) TModality
Id TermT n
tA Maybe (ScopedTermT n)
forall a. Maybe a
Nothing
            (NameBinder n l -> TermT l -> ScopedTermT n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder n l
zBinder
              (Binder
-> TModality
-> TermT l
-> Maybe (ScopedTermT l)
-> ScopedTermT l
-> TermT l
forall (n :: S).
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> ScopedTermT n
-> TermT n
typeFunT (Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing) TModality
Id TermT l
idType Maybe (ScopedTermT l)
forall a. Maybe a
Nothing
                (NameBinder l l
-> AST NameBinder (AnnSig TypeInfo TermSig) l -> ScopedTermT l
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder l l
pBinder AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S). TermT n
universeT)))