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

-- | The meta-parameter layer check.
--
-- The type theory implemented in rzk separates a /meta-theoretic parameter
-- layer/ from the object theory (RSTT proper): see §3.2 of the Rzk paper
-- (Kudasov, Sim, Ahrens, \"Rzk: a Proof Assistant for Synthetic
-- ∞-Categories\", <https://arxiv.org/abs/2607.12207 arXiv:2607.12207>),
-- where a statement is abstracted over a context of schematic cube, tope,
-- and type parameters. The checker did not enforce responsible use of
-- this layer. Per declaration, the /meta prefix/ is the
-- parameter prefix up to and including the last parameter whose type lives
-- outside RSTT proper: a universe, @CUBE@, @TOPE@, or a Π-type quantifying
-- over or landing in one of those. Interleaved object parameters are swept
-- in, which only strengthens the check.
--
-- The discipline: the meta prefix must be fully supplied wherever the
-- declaration is used at an object-level position; unsaturated use at a
-- meta-typed position is legitimate macro-level plumbing and stays allowed.
-- Then the development reads as a family of object-theory definitions, one
-- per meta instantiation.
--
-- Positions are classified structurally, on the elaborated term:
--
-- - the root of a declaration's type and value is meta (a definition may
--   alias a schema), and a λ-body inherits its λ's position (the value's
--   leading λs are the declaration's own parameters);
-- - an application argument is meta when the function's Π-domain at that
--   position is meta-shaped (the receiver declared a schema parameter);
-- - the components of type formers are meta (types are the schema layer),
--   except the endpoints of an identity type, which are terms;
-- - everything else (pair components, projections, @recOR@ branches, a
--   @let@-bound value, …) is an object position.
--
-- The strict rule (the default, see 'MetaPrefixSensitivity') additionally
-- requires an unsaturated schema argument to sit within a /top-level/
-- receiver's meta prefix. This also polices meta-shaped domains that only
-- arise by instantiating a receiver's object parameters with large types
-- (as in composing schema-level implications with a generic @comp@); such
-- uses are emitted with the distinct code 'MetaPrefixStrictOnly', so the
-- structural sensitivity can silence them without losing the rest.
--
-- Known blind spot: under type-in-type, an impredicative instantiation can
-- forge a meta-shaped argument domain out of an object parameter — with
-- @g : (X : U) → X → X@, in @g ((X : U) → X → X) my-id@ the second
-- domain is meta-shaped only because @X@ was instantiated with a large
-- type. The structural sensitivity reads such a position as meta and stays
-- silent. The strict default flags it when the argument falls outside the
-- receiver's meta prefix (as here), but a forgery landing /within/ the
-- prefix, or behind a λ-bound receiver, still passes: deciding whether an
-- instantiation is genuinely impredicative is level inference, a separate
-- (planned) analysis, not this check.
module Rzk.TypeCheck.MetaPrefix (
  metaPrefixOf,
  isMetaType,
  recordMetaPrefixUses,
) where

import           Control.Monad            (forM_, when)
import           Control.Monad.Except     (catchError)
import           Control.Monad.Reader     (ask, asks)
import           Data.Bifoldable          (bifoldr)
import           Data.Maybe               (fromMaybe)

import           Control.Monad.Foil       (Distinct)
import qualified Control.Monad.Foil       as Foil
import           Control.Monad.Free.Foil  (AST (Node, Var))

import           Control.Monad.Free.Foil.Annotated (AnnSig (..))
import           Language.Rzk.Foil.Names  (TModality (..), TypeInfo (..),
                                           VarIdent, binderName)
import           Language.Rzk.Foil.Syntax
import           Rzk.TypeCheck.Context
import           Rzk.TypeCheck.Eval
import           Rzk.TypeCheck.Monad

-- * Classifying types

-- | Does this type live outside RSTT proper — is it a universe, @CUBE@,
-- @TOPE@, or a Π-type that quantifies over or lands in one of those? This
-- covers a family into a universe (@A → U@, a tope family) and a schematic
-- type such as @(X : U) → X → X@ (predicatively both are large). A
-- parameter of such a type is a meta parameter. Never throws; an
-- unanswerable probe reads as object.
isMetaType :: Distinct n => TermT n -> TypeCheck n Bool
isMetaType :: forall (n :: S). Distinct n => TermT n -> TypeCheck n Bool
isMetaType TermT n
t = (ReaderT
   (Context n)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   Bool
 -> (TypeErrorInScopedContext
     -> ReaderT
          (Context n)
          (ExceptT TypeErrorInScopedContext (State CheckLog))
          Bool)
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      Bool)
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         Bool)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  Bool
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         Bool)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     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
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False) (ReaderT
   (Context n)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   Bool
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      Bool)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a b. (a -> b) -> a -> b
$ do
  t' <- TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
headView TermT n
t
  case t' of
    UniverseT{}     -> Bool
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    UniverseCubeT{} -> Bool
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    UniverseTopeT{} -> Bool
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    TypeFunT TypeInfo (TermT n)
_ Binder
orig TModality
md TermT n
param Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret -> do
      paramMeta <- TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall (n :: S). Distinct n => TermT n -> TypeCheck n Bool
isMetaType TermT n
param
      if paramMeta
        then pure True
        else inScope orig md param ret isMetaType
    TermT n
_               -> Bool
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

-- | The length of the meta prefix of a declaration with this type: the
-- number of leading parameters up to and including the last meta one
-- (0 when there is none). Never throws.
metaPrefixOf :: Distinct n => TermT n -> TypeCheck n Int
metaPrefixOf :: forall (n :: S). Distinct n => TermT n -> TypeCheck n Int
metaPrefixOf TermT n
ty = (ReaderT
   (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) Int
 -> (TypeErrorInScopedContext
     -> ReaderT
          (Context n)
          (ExceptT TypeErrorInScopedContext (State CheckLog))
          Int)
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      Int)
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         Int)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) Int
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) Int
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) Int
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         Int)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) Int
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
_ -> 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) (ReaderT
   (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) Int
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      Int)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) Int
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) Int
forall a b. (a -> b) -> a -> b
$ Int
-> Int
-> TermT n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) Int
forall (l :: S).
Distinct l =>
Int -> Int -> TermT l -> TypeCheck l Int
go Int
1 Int
0 TermT n
ty
  where
    go :: Distinct l => Int -> Int -> TermT l -> TypeCheck l Int
    go :: forall (l :: S).
Distinct l =>
Int -> Int -> TermT l -> TypeCheck l Int
go Int
pos Int
acc TermT l
t = TermT l -> TypeCheck l (TermT l)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
headView TermT l
t TypeCheck l (TermT l)
-> (TermT l
    -> ReaderT
         (Context l)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         Int)
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) Int
forall a b.
ReaderT
  (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      TypeFunT TypeInfo (TermT l)
_ Binder
orig TModality
md TermT l
param Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) l)
_mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
ret -> do
        meta <- TermT l -> TypeCheck l Bool
forall (n :: S). Distinct n => TermT n -> TypeCheck n Bool
isMetaType TermT l
param
        let acc' = if Bool
meta then Int
pos else Int
acc
        inScope orig md param ret (go (pos + 1) acc')
      TermT l
_ -> Int
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) Int
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
acc

-- | The head of a type, for classification: syntactically if the head is
-- already informative, through WHNF otherwise (a defined name such as
-- @FunExt@ must unfold). Restrictions are stripped either way; a boundary
-- does not change which layer a type lives in.
headView :: Distinct n => TermT n -> TypeCheck n (TermT n)
headView :: forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
headView TermT n
t = case TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
stripTypeRestrictions TermT n
t of
  t' :: TermT n
t'@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
t'
  t' :: TermT n
t'@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
t'
  t' :: TermT n
t'@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
t'
  t' :: TermT n
t'@TypeFunT{}      -> 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'
  t' :: TermT n
t'@TypeSigmaT{}    -> 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'
  t' :: TermT n
t'@TypeIdT{}       -> 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
t'                 -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
stripTypeRestrictions (TermT n -> TermT n)
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TermT n
t'

-- * The use-site walk

-- | How a position is classified under the two candidate rules.
data PosKind = MetaPos | ObjectPos
  deriving (PosKind -> PosKind -> Bool
(PosKind -> PosKind -> Bool)
-> (PosKind -> PosKind -> Bool) -> Eq PosKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PosKind -> PosKind -> Bool
== :: PosKind -> PosKind -> Bool
$c/= :: PosKind -> PosKind -> Bool
/= :: PosKind -> PosKind -> Bool
Eq)

data Positions = Positions
  { Positions -> PosKind
posStructural :: PosKind
  , Positions -> PosKind
posStrict     :: PosKind
  }

rootPositions, typePositions, objectPositions :: Positions
rootPositions :: Positions
rootPositions   = PosKind -> PosKind -> Positions
Positions PosKind
MetaPos PosKind
MetaPos
typePositions :: Positions
typePositions   = PosKind -> PosKind -> Positions
Positions PosKind
MetaPos PosKind
MetaPos
objectPositions :: Positions
objectPositions = PosKind -> PosKind -> Positions
Positions PosKind
ObjectPos PosKind
ObjectPos

-- | Walk a declaration's elaborated type and value, warning about every
-- use of a top-level name that supplies fewer arguments than its meta
-- prefix at an object-level position. Advisory: never throws, and runs
-- silently so WHNF probes do not trace.
recordMetaPrefixUses
  :: forall n. Distinct n
  => VarIdent -> TermT n -> Maybe (TermT n) -> TypeCheck n ()
recordMetaPrefixUses :: forall (n :: S).
Distinct n =>
VarIdent -> TermT n -> Maybe (TermT n) -> TypeCheck n ()
recordMetaPrefixUses VarIdent
defName TermT n
ty Maybe (TermT n)
mval =
  (Context n -> MetaPrefixSensitivity)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     MetaPrefixSensitivity
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context n -> MetaPrefixSensitivity
forall (n :: S). Context n -> MetaPrefixSensitivity
ctxMetaPrefixSensitivity ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  MetaPrefixSensitivity
-> (MetaPrefixSensitivity
    -> 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
    MetaPrefixSensitivity
MetaPrefixOff -> ()
-> 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 ()
    MetaPrefixSensitivity
_ -> Verbosity
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S) a. Verbosity -> TypeCheck n a -> TypeCheck n a
localVerbosity Verbosity
Silent (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
$ (ReaderT
   (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
 -> (TypeErrorInScopedContext
     -> ReaderT
          (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
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
_ -> ()
-> 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 ()) (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
$ do
      Positions
-> TermT n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
rootPositions TermT n
ty
      (TermT n
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> Maybe (TermT n)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Positions
-> TermT n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
rootPositions) Maybe (TermT n)
mval
  where
    go :: forall l. Distinct l => Positions -> TermT l -> TypeCheck l ()
    go :: forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
pos TermT l
t = case TermT l
t of
      Var Name l
v -> Positions -> Name l -> Int -> TypeCheck l ()
forall (l :: S). Positions -> Name l -> Int -> TypeCheck l ()
checkHead Positions
pos Name l
v Int
0

      AppT{} -> do
        let (TermT l
h, [(TermT l, TermT l)]
args) = TermT l -> [(TermT l, TermT l)] -> (TermT l, [(TermT l, TermT l)])
forall (n :: S).
TermT n -> [(TermT n, TermT n)] -> (TermT n, [(TermT n, TermT n)])
collectSpine TermT l
t []
        mk <- case TermT l
h of
          Var Name l
v -> do
            ctx <- ReaderT
  (Context l)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Context l)
forall r (m :: * -> *). MonadReader r m => m r
ask
            let info = Name l -> Context l -> VarInfo l
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name l
v Context l
ctx
            checkHead pos v (length args)
            pure (if varIsTopLevel info then Just (varMetaPrefix info) else Nothing)
          TermT l
_ -> do
            Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
objectPositions TermT l
h
            Maybe Int
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe Int)
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Int
forall a. Maybe a
Nothing
        forM_ (zip [1 :: Int ..] args) $ \(Int
i, (TermT l
fnode, TermT l
arg)) -> do
          domMeta <- TermT l -> TypeCheck l Bool
forall (n :: S). Distinct n => TermT n -> TypeCheck n Bool
domainIsMeta TermT l
fnode
          let strict = case Maybe Int
mk of
                Just Int
k | Bool
domMeta Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
k -> PosKind
MetaPos
                Maybe Int
_                          -> PosKind
ObjectPos
          go (Positions (if domMeta then MetaPos else ObjectPos) strict) arg

      LambdaT TypeInfo (TermT l)
info Binder
orig Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) l) (TermT l))
mparam ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
body -> do
        (mdom, md) <- case Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) l) (TermT l))
mparam of
          Just (LambdaParam TModality
m TermT l
ty' Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) l)
_mtope) -> do
            Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
typePositions TermT l
ty'
            (Maybe (TermT l), TModality)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l), TModality)
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT l -> Maybe (TermT l)
forall a. a -> Maybe a
Just TermT l
ty', TModality
m)
          -- A bare λ: the domain of its own Π-type.
          Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) l) (TermT l))
Nothing -> do
            dom <- TermT l -> TypeCheck l (Maybe (TermT l))
forall (l :: S).
Distinct l =>
TermT l -> TypeCheck l (Maybe (TermT l))
funDomain (TypeInfo (TermT l) -> TermT l
forall term. TypeInfo term -> term
infoType TypeInfo (TermT l)
info)
            pure (dom, Id)
        inScope orig md (fromMaybe universeT mdom) body (go pos)

      TypeFunT TypeInfo (TermT l)
_ Binder
orig TModality
md TermT l
param Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) l)
_mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
ret -> do
        Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
typePositions TermT l
param
        Binder
-> TModality
-> TermT l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    AST NameBinder (AnnSig TypeInfo TermSig) l -> TypeCheck l ())
-> TypeCheck l ()
forall (sig :: * -> * -> *) (n :: S) a.
(Bifunctor sig, Distinct n) =>
Binder
-> TModality
-> TermT n
-> ScopedAST NameBinder sig n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    AST NameBinder sig l -> TypeCheck l a)
-> TypeCheck n a
inScope Binder
orig TModality
md TermT l
param ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
ret (Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
typePositions)

      TypeSigmaT TypeInfo (TermT l)
_ Binder
orig TModality
md TermT l
a ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
bscope -> do
        Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
typePositions TermT l
a
        Binder
-> TModality
-> TermT l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    AST NameBinder (AnnSig TypeInfo TermSig) l -> TypeCheck l ())
-> TypeCheck l ()
forall (sig :: * -> * -> *) (n :: S) a.
(Bifunctor sig, Distinct n) =>
Binder
-> TModality
-> TermT n
-> ScopedAST NameBinder sig n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    AST NameBinder sig l -> TypeCheck l a)
-> TypeCheck n a
inScope Binder
orig TModality
md TermT l
a ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
bscope (Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
typePositions)

      -- The endpoints are terms; storing an unsaturated schema in an
      -- identity type is an object-level use.
      TypeIdT TypeInfo (TermT l)
_ TermT l
a Maybe (TermT l)
mtA TermT l
b -> do
        Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
objectPositions TermT l
a
        (TermT l -> TypeCheck l ()) -> Maybe (TermT l) -> TypeCheck l ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
typePositions) Maybe (TermT l)
mtA
        Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
objectPositions TermT l
b

      TypeRestrictedT TypeInfo (TermT l)
_ TermT l
ty' [(TermT l, TermT l)]
rs -> do
        Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
typePositions TermT l
ty'
        [(TermT l, TermT l)]
-> ((TermT l, TermT l) -> TypeCheck l ()) -> TypeCheck l ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(TermT l, TermT l)]
rs (((TermT l, TermT l) -> TypeCheck l ()) -> TypeCheck l ())
-> ((TermT l, TermT l) -> TypeCheck l ()) -> TypeCheck l ()
forall a b. (a -> b) -> a -> b
$ \(TermT l
_tope, TermT l
term) -> Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
objectPositions TermT l
term

      LetT TypeInfo (TermT l)
_ Binder
orig Maybe (TermT l)
manno TermT l
value ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
body -> do
        (TermT l -> TypeCheck l ()) -> Maybe (TermT l) -> TypeCheck l ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
typePositions) Maybe (TermT l)
manno
        Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
objectPositions TermT l
value
        let valueType :: Maybe (TermT l)
valueType = case TermT l -> Maybe (TypeInfo (TermT l))
forall (n :: S). TermT n -> Maybe (TypeInfo (TermT n))
typeInfoOf TermT l
value of
              Just TypeInfo (TermT l)
valueInfo -> TermT l -> Maybe (TermT l)
forall a. a -> Maybe a
Just (TypeInfo (TermT l) -> TermT l
forall term. TypeInfo term -> term
infoType TypeInfo (TermT l)
valueInfo)
              Maybe (TypeInfo (TermT l))
Nothing        -> Maybe (TermT l)
manno
        Binder
-> TModality
-> TermT l
-> Maybe (TermT l)
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
-> (forall (l :: S).
    (DExt l l, Distinct l) =>
    AST NameBinder (AnnSig TypeInfo TermSig) l -> TypeCheck l ())
-> TypeCheck l ()
forall (sig :: * -> * -> *) (n :: S) a.
(Bifunctor sig, Distinct n) =>
Binder
-> TModality
-> TermT n
-> Maybe (TermT n)
-> ScopedAST NameBinder sig n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    AST NameBinder sig l -> TypeCheck l a)
-> TypeCheck n a
inScopeWith Binder
orig TModality
Id (TermT l -> Maybe (TermT l) -> TermT l
forall a. a -> Maybe a -> a
fromMaybe TermT l
forall (n :: S). TermT n
universeT Maybe (TermT l)
valueType) (TermT l -> Maybe (TermT l)
forall a. a -> Maybe a
Just TermT l
value) ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
body (Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
pos)

      LetModT TypeInfo (TermT l)
_ Binder
orig TModality
_nu TModality
mu Maybe (TermT l)
manno Maybe (TermT l)
mmotive TermT l
value ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
body -> do
        (TermT l -> TypeCheck l ()) -> Maybe (TermT l) -> TypeCheck l ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
typePositions) Maybe (TermT l)
manno
        (TermT l -> TypeCheck l ()) -> Maybe (TermT l) -> TypeCheck l ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
typePositions) Maybe (TermT l)
mmotive
        Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
objectPositions TermT l
value
        unwrapped <- case TermT l -> Maybe (TypeInfo (TermT l))
forall (n :: S). TermT n -> Maybe (TypeInfo (TermT n))
typeInfoOf TermT l
value of
          Maybe (TypeInfo (TermT l))
Nothing        -> Maybe (TermT l) -> TypeCheck l (Maybe (TermT l))
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (TermT l)
forall a. Maybe a
Nothing
          Just TypeInfo (TermT l)
valueInfo -> TermT l -> TypeCheck l (Maybe (TermT l))
forall (l :: S). TermT l -> TypeCheck l (Maybe (TermT l))
modalDomain (TypeInfo (TermT l) -> TermT l
forall term. TypeInfo term -> term
infoType TypeInfo (TermT l)
valueInfo)
        inScope orig mu (fromMaybe universeT unwrapped) body (go pos)

      Node (AnnSig TypeInfo (TermT l)
_ TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) l) (TermT l)
f) ->
        (TermT l -> TypeCheck l ()) -> [TermT l] -> TypeCheck l ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Positions -> TermT l -> TypeCheck l ()
forall (l :: S).
Distinct l =>
Positions -> TermT l -> TypeCheck l ()
go Positions
objectPositions) ((ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
 -> [TermT l] -> [TermT l])
-> (TermT l -> [TermT l] -> [TermT l])
-> [TermT l]
-> TermSig
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) l) (TermT l)
-> [TermT l]
forall a c b.
(a -> c -> c) -> (b -> c -> c) -> c -> TermSig a b -> c
forall (p :: * -> * -> *) a c b.
Bifoldable p =>
(a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
bifoldr (\ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
_ [TermT l]
acc -> [TermT l]
acc) (:) [] TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) l) (TermT l)
f)

    -- An unsaturated top-level head at an object position warns; at a
    -- position only the strict rule rejects, the warning is marked so.
    checkHead :: forall l. Positions -> Foil.Name l -> Int -> TypeCheck l ()
    checkHead :: forall (l :: S). Positions -> Name l -> Int -> TypeCheck l ()
checkHead Positions
pos Name l
v Int
nargs = do
      ctx <- ReaderT
  (Context l)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Context l)
forall r (m :: * -> *). MonadReader r m => m r
ask
      let info = Name l -> Context l -> VarInfo l
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name l
v Context l
ctx
          k = VarInfo l -> Int
forall (n :: S). VarInfo n -> Int
varMetaPrefix VarInfo l
info
      when (varIsTopLevel info && k > nargs) $ do
        sensitivity <- asks ctxMetaPrefixSensitivity
        let mrule = case (Positions -> PosKind
posStructural Positions
pos, Positions -> PosKind
posStrict Positions
pos) of
              (PosKind
ObjectPos, PosKind
_) -> MetaPrefixRule -> Maybe MetaPrefixRule
forall a. a -> Maybe a
Just MetaPrefixRule
MetaPrefixBoth
              (PosKind
MetaPos, PosKind
ObjectPos)
                | MetaPrefixSensitivity
MetaPrefixStrict <- MetaPrefixSensitivity
sensitivity -> MetaPrefixRule -> Maybe MetaPrefixRule
forall a. a -> Maybe a
Just MetaPrefixRule
MetaPrefixStrictOnly
              (PosKind, PosKind)
_              -> Maybe MetaPrefixRule
forall a. Maybe a
Nothing
        forM_ mrule $ \MetaPrefixRule
rule -> do
          loc <- (Context l -> Maybe LocationInfo)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe LocationInfo)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context l -> Maybe LocationInfo
forall (n :: S). Context n -> Maybe LocationInfo
ctxLocation
          recordCheckWarning $ MetaPrefixWarning
            defName
            (fromMaybe "_" (binderName (varOrig info)))
            nargs
            k
            rule
            loc

    -- Is the Π-domain of this function node meta-shaped?
    domainIsMeta :: forall l. Distinct l => TermT l -> TypeCheck l Bool
    domainIsMeta :: forall (n :: S). Distinct n => TermT n -> TypeCheck n Bool
domainIsMeta TermT l
f = (ReaderT
   (Context l)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   Bool
 -> (TypeErrorInScopedContext
     -> ReaderT
          (Context l)
          (ExceptT TypeErrorInScopedContext (State CheckLog))
          Bool)
 -> ReaderT
      (Context l)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      Bool)
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context l)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         Bool)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  (Context l)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  Bool
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context l)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         Bool)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a.
ReaderT
  (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a)
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (\TypeErrorInScopedContext
_ -> Bool
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False) (ReaderT
   (Context l)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   Bool
 -> ReaderT
      (Context l)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      Bool)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a b. (a -> b) -> a -> b
$ do
      tf <- TermT l -> TypeCheck l (TermT l)
forall (n :: S). TermT n -> TypeCheck n (TermT n)
typeOfUncomputed TermT l
f
      headView tf >>= \case
        TypeFunT TypeInfo (TermT l)
_ Binder
_ TModality
_ TermT l
dom Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) l)
_ ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
_ -> TermT l
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall (n :: S). Distinct n => TermT n -> TypeCheck n Bool
isMetaType TermT l
dom
        TermT l
_                      -> Bool
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

    funDomain :: forall l. Distinct l => TermT l -> TypeCheck l (Maybe (TermT l))
    funDomain :: forall (l :: S).
Distinct l =>
TermT l -> TypeCheck l (Maybe (TermT l))
funDomain TermT l
tf = (ReaderT
   (Context l)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   (Maybe (TermT l))
 -> (TypeErrorInScopedContext
     -> ReaderT
          (Context l)
          (ExceptT TypeErrorInScopedContext (State CheckLog))
          (Maybe (TermT l)))
 -> ReaderT
      (Context l)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe (TermT l)))
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context l)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe (TermT l)))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  (Context l)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Maybe (TermT l))
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context l)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe (TermT l)))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall a.
ReaderT
  (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a)
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (\TypeErrorInScopedContext
_ -> Maybe (TermT l)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (TermT l)
forall a. Maybe a
Nothing) (ReaderT
   (Context l)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   (Maybe (TermT l))
 -> ReaderT
      (Context l)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe (TermT l)))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall a b. (a -> b) -> a -> b
$
      TermT l -> TypeCheck l (TermT l)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
headView TermT l
tf TypeCheck l (TermT l)
-> (TermT l
    -> ReaderT
         (Context l)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe (TermT l)))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall a b.
ReaderT
  (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        TypeFunT TypeInfo (TermT l)
_ Binder
_ TModality
_ TermT l
dom Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) l)
_ ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
_ -> Maybe (TermT l)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT l -> Maybe (TermT l)
forall a. a -> Maybe a
Just TermT l
dom)
        TermT l
_                      -> Maybe (TermT l)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (TermT l)
forall a. Maybe a
Nothing

    modalDomain :: forall l. TermT l -> TypeCheck l (Maybe (TermT l))
    modalDomain :: forall (l :: S). TermT l -> TypeCheck l (Maybe (TermT l))
modalDomain TermT l
tv = (ReaderT
   (Context l)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   (Maybe (TermT l))
 -> (TypeErrorInScopedContext
     -> ReaderT
          (Context l)
          (ExceptT TypeErrorInScopedContext (State CheckLog))
          (Maybe (TermT l)))
 -> ReaderT
      (Context l)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe (TermT l)))
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context l)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe (TermT l)))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  (Context l)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Maybe (TermT l))
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context l)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe (TermT l)))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall a.
ReaderT
  (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a)
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (\TypeErrorInScopedContext
_ -> Maybe (TermT l)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (TermT l)
forall a. Maybe a
Nothing) (ReaderT
   (Context l)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   (Maybe (TermT l))
 -> ReaderT
      (Context l)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe (TermT l)))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall a b. (a -> b) -> a -> b
$
      Maybe (TermT l)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (TermT l)
 -> ReaderT
      (Context l)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe (TermT l)))
-> Maybe (TermT l)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
forall a b. (a -> b) -> a -> b
$ case TermT l -> TermT l
forall (n :: S). TermT n -> TermT n
stripTypeRestrictions TermT l
tv of
        TypeModalT TypeInfo (TermT l)
_ TModality
_ TermT l
a -> TermT l -> Maybe (TermT l)
forall a. a -> Maybe a
Just TermT l
a
        TermT l
_                -> Maybe (TermT l)
forall a. Maybe a
Nothing

collectSpine :: TermT n -> [(TermT n, TermT n)] -> (TermT n, [(TermT n, TermT n)])
collectSpine :: forall (n :: S).
TermT n -> [(TermT n, TermT n)] -> (TermT n, [(TermT n, TermT n)])
collectSpine (AppT TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
_ AST NameBinder (AnnSig TypeInfo TermSig) n
f AST NameBinder (AnnSig TypeInfo TermSig) n
x) [(AST NameBinder (AnnSig TypeInfo TermSig) n,
  AST NameBinder (AnnSig TypeInfo TermSig) n)]
acc = 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, [(TermT n, TermT n)])
collectSpine AST NameBinder (AnnSig TypeInfo TermSig) n
f ((AST NameBinder (AnnSig TypeInfo TermSig) n
f, AST NameBinder (AnnSig TypeInfo TermSig) n
x) (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 a. a -> [a] -> [a]
: [(AST NameBinder (AnnSig TypeInfo TermSig) n,
  AST NameBinder (AnnSig TypeInfo TermSig) n)]
acc)
collectSpine AST NameBinder (AnnSig TypeInfo TermSig) n
h [(AST NameBinder (AnnSig TypeInfo TermSig) n,
  AST NameBinder (AnnSig TypeInfo TermSig) n)]
acc            = (AST NameBinder (AnnSig TypeInfo TermSig) n
h, [(AST NameBinder (AnnSig TypeInfo TermSig) n,
  AST NameBinder (AnnSig TypeInfo TermSig) n)]
acc)