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

-- | Unification, which in rzk is really subtyping: an extension type's faces, a
-- shape's tope and the variance of the position all take part.
module Rzk.TypeCheck.Unify where

import           Control.Monad            (forM_, unless, when)
import           Control.Monad.Except     (catchError, throwError)
import           Control.Monad.Reader     (asks)
import           Data.Maybe               (fromMaybe)
import           Data.Tuple               (swap)

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

import           Language.Rzk.Foil.Syntax
import           Language.Rzk.Foil.Names (Binder, TModality (..),
                                           TypeInfo (..))
import           Rzk.TypeCheck.Context
import           Rzk.TypeCheck.Display (panicImpossible)
import           Rzk.TypeCheck.Error
import           Rzk.TypeCheck.Eval
import           Rzk.TypeCheck.Monad
import           Rzk.TypeCheck.NbE (Conversion (..), nbeConvertible)

-- | Open two scoped terms under /one/ binder, so that the two sides of a
-- comparison are compared as functions of the same variable.
inScope2
  :: Distinct n
  => Binder -> TModality -> TermT n
  -> ScopedTermT n -> ScopedTermT n
  -> (forall l. (DExt n l, Distinct l)
        => NameBinder n l -> TermT l -> TermT l -> TypeCheck l a)
  -> TypeCheck n a
inScope2 :: forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> ScopedTermT n
-> ScopedTermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TermT l -> TermT l -> TypeCheck l a)
-> TypeCheck n a
inScope2 Binder
orig TModality
md TermT n
ty ScopedTermT n
s1 ScopedTermT n
s2 forall (l :: S).
(DExt n l, Distinct l) =>
NameBinder n l -> TermT l -> TermT l -> TypeCheck l a
k = 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
  withScopedT2 scope s1 s2 $ \NameBinder n l
binder TermT l
body1 TermT l
body2 ->
    NameBinder n l
-> Binder
-> TModality
-> TermT n
-> Maybe (TermT n)
-> TypeCheck l a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (n :: S) (l :: S) a.
(Distinct n, DExt n l) =>
NameBinder n l
-> Binder
-> TModality
-> TermT n
-> Maybe (TermT n)
-> TypeCheck l a
-> TypeCheck n a
underBinder NameBinder n l
binder Binder
orig TModality
md TermT n
ty Maybe (TermT n)
forall a. Maybe a
Nothing (NameBinder n l -> TermT l -> TermT l -> TypeCheck l a
forall (l :: S).
(DExt n l, Distinct l) =>
NameBinder n l -> TermT l -> TermT l -> TypeCheck l a
k NameBinder n l
binder TermT l
body1 TermT l
body2)

-- | α-equivalence in the ambient scope.
alphaEq :: Distinct n => TermT n -> TermT n -> TypeCheck n Bool
alphaEq :: forall (n :: S).
Distinct n =>
TermT n -> TermT n -> TypeCheck n Bool
alphaEq TermT n
l TermT n
r = 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 (alphaEqT scope l r)

-- | Run @check super sub@ on the pair @(expected, actual)@, oriented by the
-- ambient variance. Under 'Covariant' the expected type is the supertype and
-- under 'Contravariant' the actual one is. 'Invariant' is normally handled
-- upstream by running both directions; we run both here as well, for safety.
bySubtyping
  :: (TermT n -> TermT n -> TypeCheck n ())
  -> TermT n -> TermT n -> TypeCheck n ()
bySubtyping :: forall (n :: S).
(TermT n -> TermT n -> TypeCheck n ())
-> TermT n -> TermT n -> TypeCheck n ()
bySubtyping TermT n -> TermT n -> TypeCheck n ()
check TermT n
expected TermT n
actual = (Context n -> Covariance)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Covariance
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context n -> Covariance
forall (n :: S). Context n -> Covariance
ctxCovariance ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  Covariance
-> (Covariance -> TypeCheck n ()) -> TypeCheck 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
  Covariance
Covariant     -> TermT n -> TermT n -> TypeCheck n ()
check TermT n
expected TermT n
actual
  Covariance
Contravariant -> TermT n -> TermT n -> TypeCheck n ()
check TermT n
actual TermT n
expected
  Covariance
Invariant     -> TermT n -> TermT n -> TypeCheck n ()
check TermT n
expected TermT n
actual TypeCheck n () -> TypeCheck n () -> TypeCheck n ()
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
>> TermT n -> TermT n -> TypeCheck n ()
check TermT n
actual TermT n
expected

-- | The domain of a shape-indexed function is contravariant, so the subtype's
-- domain tope has to hold wherever the supertype's does. Shared by Π-types
-- and by the lambdas that inhabit them.
domainEntails :: Distinct n => TermT n -> TermT n -> TypeCheck n ()
domainEntails :: forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
domainEntails TermT n
superTope TermT n
subTope = TermT n -> TypeCheck n () -> TypeCheck n ()
forall (n :: S) a.
Distinct n =>
TermT n -> TypeCheck n a -> TypeCheck n a
localTope TermT n
superTope (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TypeCheck n ()
contextEntails TermT n
subTope

unifyTopes :: Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTopes :: forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTopes TermT n
l TermT n
r = do
  equiv <- Bool -> Bool -> Bool
(&&)
    (Bool -> Bool -> Bool)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TermT n -> ModalTope n
forall (n :: S). TermT n -> ModalTope n
plainTope TermT n
l] [ModalTope n]
-> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall (n :: S).
Distinct n =>
[ModalTope n] -> TermT n -> TypeCheck n Bool
`entailM` TermT n
r
    ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Bool -> Bool)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall a b.
ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (a -> b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [TermT n -> ModalTope n
forall (n :: S). TermT n -> ModalTope n
plainTope TermT n
r] [ModalTope n]
-> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall (n :: S).
Distinct n =>
[ModalTope n] -> TermT n -> TypeCheck n Bool
`entailM` TermT n
l
  unless equiv $
    issueTypeError (TypeErrorTopesNotEquivalent l r)

unify
  :: Distinct n
  => Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
unify :: forall (n :: S).
Distinct n =>
Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
unify Maybe (TermT n)
mterm TermT n
expected TermT n
actual = TypeCheck n ()
performUnification TypeCheck n ()
-> (TypeErrorInScopedContext -> TypeCheck n ()) -> TypeCheck n ()
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
typeError -> do
  TypeCheck n () -> TypeCheck n () -> TypeCheck n ()
forall (n :: S).
Distinct n =>
TypeCheck n () -> TypeCheck n () -> TypeCheck n ()
inAllSubContexts (TypeErrorInScopedContext -> TypeCheck n ()
forall a.
TypeErrorInScopedContext
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TypeErrorInScopedContext
typeError) TypeCheck n ()
performUnification
  where
    performUnification :: TypeCheck n ()
performUnification = Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
forall (n :: S).
Distinct n =>
Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
unifyInCurrentContext Maybe (TermT n)
mterm TermT n
expected TermT n
actual

-- | The syntactic fast path.
--
-- α-equivalence, not the structural equality the old representation used: two
-- terms that differ only in a binder's name are the same term, and saying so here
-- saves the whole unification below.
unifyViaDecompose :: Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyViaDecompose :: forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyViaDecompose TermT n
expected TermT n
actual = do
  same <- TermT n -> TermT n -> TypeCheck n Bool
forall (n :: S).
Distinct n =>
TermT n -> TermT n -> TypeCheck n Bool
alphaEq TermT n
expected TermT n
actual
  if same
    then return ()
    else do
      -- The NbE fast path: a shared-evaluation βδη-conversion check over the
      -- context-insensitive fragment. 'Convertible' is definite (see the
      -- module's soundness note); 'DontKnow' is not a refutation, and
      -- unification proceeds unchanged. It must run /before/ the application
      -- decomposition below: decomposing @f x@ against @g y@ compares the
      -- arguments pairwise, which for βδ-equal but structurally different
      -- applications creates false subgoals (e.g. @16 =? 128@ from
      -- @16 · 16 =? 128 + 128@) that the old path then grinds through only to
      -- fail and unwind.
      fastPath <- nbeConvertible expected actual
      case fastPath of
        Conversion
Convertible -> ()
-> 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 ()
        Conversion
DontKnow -> case (TermT n
expected, TermT n
actual) of
          (AppT TypeInfo (TermT n)
_ TermT n
f TermT n
x, AppT TypeInfo (TermT n)
_ TermT n
g TermT n
y) -> do
            Maybe (TermT n)
-> TermT n
-> TermT n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
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
f TermT n
g
            Covariance
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S) a. Covariance -> TypeCheck n a -> TypeCheck n a
setVariance Covariance
Invariant (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
$ Maybe (TermT n)
-> TermT n
-> TermT n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
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
x TermT n
y
          (TermT n, TermT n)
_ -> TypeError n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (String -> TypeError n
forall (n :: S). String -> TypeError n
TypeErrorOther String
"cannot decompose")

unifyTypes :: Distinct n => TermT n -> TermT n -> TermT n -> TypeCheck n ()
unifyTypes :: forall (n :: S).
Distinct n =>
TermT n -> TermT n -> TermT n -> TypeCheck n ()
unifyTypes = 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) -> TermT n -> TermT n -> TypeCheck n ())
-> (TermT n -> Maybe (TermT n))
-> TermT n
-> TermT n
-> TermT n
-> TypeCheck n ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just

unifyTerms :: Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTerms :: forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTerms = 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

checkCoherence
  :: Distinct n
  => (TermT n, TermT n) -> (TermT n, TermT n) -> TypeCheck n ()
checkCoherence :: forall (n :: S).
Distinct n =>
(TermT n, TermT n) -> (TermT n, TermT n) -> TypeCheck n ()
checkCoherence (TermT n
ltope, TermT n
lterm) (TermT n
rtope, TermT n
rterm) =
  Action n -> TypeCheck n () -> TypeCheck n ()
forall (n :: S) a.
Distinct n =>
Action n -> TypeCheck n a -> TypeCheck n a
performing ((TermT n, TermT n) -> (TermT n, TermT n) -> Action n
forall (n :: S).
(TermT n, TermT n) -> (TermT n, TermT n) -> Action n
ActionCheckCoherence (TermT n
ltope, TermT n
lterm) (TermT n
rtope, TermT n
rterm)) (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$
    TermT n -> TypeCheck n () -> TypeCheck n ()
forall (n :: S) a.
Distinct n =>
TermT n -> TypeCheck n a -> TypeCheck n a
localTope (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeAndT TermT n
ltope TermT n
rtope) (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ do
      ltype <- 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)
typeOf TermT n
lterm   -- FIXME: why strip?
      rtype <- stripTypeRestrictions <$> typeOf rterm   -- FIXME: why strip?
      -- FIXME: do we need to unify types here or is it included in unification of terms?
      unifyTerms ltype rtype
      unifyTerms lterm rterm

unifyInCurrentContext
  :: forall n. Distinct n
  => Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
unifyInCurrentContext :: forall (n :: S).
Distinct n =>
Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
unifyInCurrentContext Maybe (TermT n)
mterm TermT n
expected TermT n
actual = Action n -> TypeCheck n () -> TypeCheck n ()
forall (n :: S) a.
Distinct n =>
Action n -> TypeCheck n a -> TypeCheck n a
performing Action n
action (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ do
  inBottom <- TypeCheck n Bool
forall (n :: S). Distinct n => TypeCheck n Bool
contextEntailsBottom
  unless inBottom $
    -- NOTE: the decomposition gives a small, but noticeable speedup
    unifyViaDecompose expected actual `catchError` \TypeErrorInScopedContext
_ -> do
      expectedVal <- TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TermT n
expected
      actualVal <- whnfT actual
      mea <- asks ctxCovariance >>= \case
        Covariance
Covariant     -> (TermT n, TermT n) -> Maybe (TermT n, TermT n)
forall a. a -> Maybe a
Just ((TermT n, TermT n) -> Maybe (TermT n, TermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n, TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n, TermT n))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (TermT n)
-> TermT n
-> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n, TermT n)
forall (n :: S).
Distinct n =>
Maybe (TermT n)
-> TermT n -> TermT n -> TypeCheck n (TermT n, TermT n)
etaMatch Maybe (TermT n)
mterm TermT n
expectedVal TermT n
actualVal
        Covariance
Contravariant -> (TermT n, TermT n) -> Maybe (TermT n, TermT n)
forall a. a -> Maybe a
Just ((TermT n, TermT n) -> Maybe (TermT n, TermT n))
-> ((TermT n, TermT n) -> (TermT n, TermT n))
-> (TermT n, TermT n)
-> Maybe (TermT n, TermT n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TermT n, TermT n) -> (TermT n, TermT n)
forall a b. (a, b) -> (b, a)
swap ((TermT n, TermT n) -> Maybe (TermT n, TermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n, TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n, TermT n))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (TermT n)
-> TermT n
-> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n, TermT n)
forall (n :: S).
Distinct n =>
Maybe (TermT n)
-> TermT n -> TermT n -> TypeCheck n (TermT n, TermT n)
etaMatch Maybe (TermT n)
mterm TermT n
actualVal TermT n
expectedVal
        Covariance
Invariant     -> Verbosity
-> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n, TermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n, TermT n))
forall (n :: S) a.
Verbosity -> String -> TypeCheck n a -> TypeCheck n a
traceTypeCheck Verbosity
Debug String
"invariant" (ReaderT
   (Context n)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   (Maybe (TermT n, TermT n))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe (TermT n, TermT n)))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n, TermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n, TermT n))
forall a b. (a -> b) -> a -> b
$ do
          -- FIXME: inefficient
          Verbosity -> String -> TypeCheck n () -> TypeCheck n ()
forall (n :: S) a.
Verbosity -> String -> TypeCheck n a -> TypeCheck n a
traceTypeCheck Verbosity
Debug String
"invariant->covariant" (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$
            Covariance -> TypeCheck n () -> TypeCheck n ()
forall (n :: S) a. Covariance -> TypeCheck n a -> TypeCheck n a
setVariance Covariance
Covariant     (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
forall (n :: S).
Distinct n =>
Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
unifyInCurrentContext Maybe (TermT n)
mterm TermT n
expectedVal TermT n
actualVal
          Verbosity -> String -> TypeCheck n () -> TypeCheck n ()
forall (n :: S) a.
Verbosity -> String -> TypeCheck n a -> TypeCheck n a
traceTypeCheck Verbosity
Debug String
"invariant->contravariant" (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$
            Covariance -> TypeCheck n () -> TypeCheck n ()
forall (n :: S) a. Covariance -> TypeCheck n a -> TypeCheck n a
setVariance Covariance
Contravariant (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
forall (n :: S).
Distinct n =>
Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
unifyInCurrentContext Maybe (TermT n)
mterm TermT n
expectedVal TermT n
actualVal
          Maybe (TermT n, TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n, 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, TermT n)
forall a. Maybe a
Nothing
      case mea of
        Maybe (TermT n, 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 ()
        -- A hole (in lenient mode) stands for a term of the expected type, so it
        -- unifies with anything; accept it rather than falling through to the
        -- dispatch below (which would panic on an unexpected term).
        Just (TermT n
expected', TermT n
actual') | TermT n -> Bool
forall (n :: S). TermT n -> Bool
isHoleT TermT n
expected' Bool -> Bool -> Bool
|| TermT n -> Bool
forall (n :: S). TermT n -> Bool
isHoleT TermT n
actual' -> () -> 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
expected', TermT n
actual') -> do
          same <- TermT n -> TermT n -> TypeCheck n Bool
forall (n :: S).
Distinct n =>
TermT n -> TermT n -> TypeCheck n Bool
alphaEq TermT n
expected' TermT n
actual'
          unless same $ dispatch expected' actual'
  where
    action :: Action n
action = case Maybe (TermT n)
mterm of
               Maybe (TermT n)
Nothing   -> TermT n -> TermT n -> Action n
forall (n :: S). TermT n -> TermT n -> Action n
ActionUnifyTerms TermT n
expected TermT n
actual
               Just TermT n
term -> TermT n -> TermT n -> TermT n -> Action n
forall (n :: S). TermT n -> TermT n -> TermT n -> Action n
ActionUnify TermT n
term TermT n
expected TermT n
actual

    dispatch :: TermT n -> TermT n -> TypeCheck n ()
    dispatch :: TermT n -> TermT n -> TypeCheck n ()
dispatch TermT n
expected' TermT n
actual' =
      case TermT n
actual' of
        RecBottomT{} -> () -> TypeCheck n ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        RecOrT TypeInfo (TermT n)
_ty [(TermT n, TermT n)]
rs' ->
          case TermT n
expected' of
            RecOrT TypeInfo (TermT n)
_ty [(TermT n, TermT n)]
rs -> [TypeCheck n ()] -> TypeCheck n ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ((TermT n, TermT n) -> (TermT n, TermT n) -> TypeCheck n ()
forall (n :: S).
Distinct n =>
(TermT n, TermT n) -> (TermT n, TermT n) -> TypeCheck n ()
checkCoherence ((TermT n, TermT n) -> (TermT n, TermT n) -> TypeCheck n ())
-> [(TermT n, TermT n)] -> [(TermT n, TermT n) -> TypeCheck n ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TermT n, TermT n)]
rs [(TermT n, TermT n) -> TypeCheck n ()]
-> [(TermT n, TermT n)] -> [TypeCheck n ()]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [(TermT n, TermT n)]
rs')
            TermT n
_ ->
              [(TermT n, TermT n)]
-> ((TermT n, TermT n) -> TypeCheck n ()) -> TypeCheck n ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(TermT n, TermT n)]
rs' (((TermT n, TermT n) -> TypeCheck n ()) -> TypeCheck n ())
-> ((TermT n, TermT n) -> TypeCheck n ()) -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ \(TermT n
tope, TermT n
term) ->
                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
expected' TermT n
term
        TermT n
_ -> TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
expected' 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)
typeOf TypeCheck n (TermT n)
-> (TermT n -> TypeCheck n ()) -> TypeCheck 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
          UniverseCubeT{} -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TypeCheck n ()
contextEntails (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
expected' TermT n
actual')
          TermT n
_ -> TermT n -> TermT n -> TypeCheck n ()
unifyStructurally TermT n
expected' TermT n
actual'

    unifyStructurally :: TermT n -> TermT n -> TypeCheck n ()
    unifyStructurally :: TermT n -> TermT n -> TypeCheck n ()
unifyStructurally TermT n
expected' TermT n
actual' = do
      -- A hole stands for a term of the expected type, so a unification that would
      -- otherwise fail is deferred when either side still contains an (unfilled)
      -- hole — including one nested in a larger term, e.g. @f ?@ checked against an
      -- extension-type boundary. The hole may also sit in the tope context rather
      -- than the terms: a hole standing for a whole shape point makes the enclosing
      -- 'recOR' split over hole-dependent faces, and a branch reduction can drop the
      -- hole from the terms while the assumed face (@π₁ ? ≤ π₂ ?@, say) still
      -- mentions it. Such a branch is only entered because the hole is unfilled, so
      -- a mismatch under it is deferred too. 'structuralHoleUnify' turns this off,
      -- keeping a structural mismatch around a hole an error.
      --
      -- A /flexible/ side is the exception 'structuralHoleUnify' does not cover:
      -- a term headed by a hole ('isHoleHeadedT') has no shape to mismatch with
      -- yet, since filling the head decides what it is. It therefore unifies with
      -- anything even under 'structuralHoleUnify'. This is what lets an
      -- eliminator whose result is a motive application be offered as a hole
      -- candidate: @ind-path ? ? ? ? ? ?@ has type @?C ?x ?p@, which fits any
      -- goal. A move is a suggestion, not a solution -- the motive and the base
      -- case are left as holes for the caller, and the result is type-checked
      -- like any other term once written.
      defer <- (Context n -> Bool) -> TypeCheck n Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context n -> Bool
forall (n :: S). Context n -> Bool
ctxDeferHoleMismatches
      topeContextHasHole <- asks (any (containsHole . tTope) . ctxTopes)
      let holePresent =
            (Bool
defer Bool -> Bool -> Bool
&& (TermT n -> Bool
forall (n :: S). TermT n -> Bool
containsHole TermT n
expected' Bool -> Bool -> Bool
|| TermT n -> Bool
forall (n :: S). TermT n -> Bool
containsHole TermT n
actual' Bool -> Bool -> Bool
|| Bool
topeContextHasHole))
              Bool -> Bool -> Bool
|| TermT n -> Bool
forall (n :: S). TermT n -> Bool
isHoleHeadedT TermT n
expected' Bool -> Bool -> Bool
|| TermT n -> Bool
forall (n :: S). TermT n -> Bool
isHoleHeadedT TermT n
actual'

          err :: TypeCheck n ()
          err
            | Bool
holePresent = () -> TypeCheck n ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            | Bool
otherwise =
                case Maybe (TermT n)
mterm of
                  Maybe (TermT n)
Nothing   -> TypeError n -> TypeCheck 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
TypeErrorUnifyTerms TermT n
expected' TermT n
actual')
                  Just TermT n
term -> TypeError n -> TypeCheck n ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError (TermT n -> TermT n -> TermT n -> TypeError n
forall (n :: S). TermT n -> TermT n -> TermT n -> TypeError n
TypeErrorUnify TermT n
term TermT n
expected' TermT n
actual')

          -- The same error, raised from inside a binder: the terms are sunk into
          -- the inner scope, which is a coercion. (The old representation had to
          -- shift each of them with @S <$>@.)
          errIn :: DExt n l => TypeCheck l ()
          errIn
            | Bool
holePresent = ()
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a.
a
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            | Bool
otherwise =
                case Maybe (TermT n)
mterm of
                  Maybe (TermT n)
Nothing -> TypeError l
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError
                    (TermT l -> TermT l -> TypeError l
forall (n :: S). TermT n -> TermT n -> TypeError n
TypeErrorUnifyTerms (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
expected') (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
actual'))
                  Just TermT n
term -> TypeError l
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError
                    (TermT l -> TermT l -> TermT l -> TypeError l
forall (n :: S). TermT n -> TermT n -> TermT n -> TypeError n
TypeErrorUnify (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
term) (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
expected') (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
actual'))

          def = do
            same <- TermT n -> TermT n -> TypeCheck n Bool
forall (n :: S).
Distinct n =>
TermT n -> TermT n -> TypeCheck n Bool
alphaEq TermT n
expected' TermT n
actual'
            unless same err

      case expected' of
        Var{} -> TypeCheck n ()
def

        UniverseT{} -> TypeCheck n ()
def
        UniverseCubeT{} -> TypeCheck n ()
def
        UniverseTopeT{} -> TypeCheck n ()
def

        TypeUnitT{} -> TypeCheck n ()
def
        UnitT{} -> () -> TypeCheck n ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- Unit always unifies!

        CubeUnitT{} -> TypeCheck n ()
def
        CubeUnitStarT{} -> TypeCheck n ()
def
        Cube2T{} -> TypeCheck n ()
def
        Cube2_0T{} -> TypeCheck n ()
def
        Cube2_1T{} -> TypeCheck n ()
def
        CubeIT{} -> TypeCheck n ()
def
        CubeI_0T{} -> TypeCheck n ()
def
        CubeI_1T{} -> TypeCheck n ()
def
        CubeProductT TypeInfo (TermT n)
_ TermT n
l TermT n
r ->
          case TermT n
actual' of
            CubeProductT TypeInfo (TermT n)
_ TermT n
l' TermT n
r' -> do
              TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTerms TermT n
l TermT n
l'
              TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTerms TermT n
r TermT n
r'
            TermT n
_ -> TypeCheck n ()
err

        PairT TypeInfo (TermT n)
_ty TermT n
l TermT n
r ->
          case TermT n
actual' of
            PairT TypeInfo (TermT n)
_ty' TermT n
l' TermT n
r' -> do
              TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTerms TermT n
l TermT n
l'
              TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTerms TermT n
r TermT n
r'
            -- one part of eta-expansion for pairs
            -- FIXME: add symmetric version!
            TermT n
_ -> TypeCheck n ()
err

        FirstT TypeInfo (TermT n)
_ty TermT n
t ->
          case TermT n
actual' of
            FirstT TypeInfo (TermT n)
_ty' TermT n
t' -> TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTerms TermT n
t TermT n
t'
            TermT n
_              -> TypeCheck n ()
err

        SecondT TypeInfo (TermT n)
_ty TermT n
t ->
          case TermT n
actual' of
            SecondT TypeInfo (TermT n)
_ty' TermT n
t' -> TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTerms TermT n
t TermT n
t'
            TermT n
_               -> TypeCheck n ()
err

        TopeTopT{}    -> TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTopes TermT n
expected' TermT n
actual'
        TopeBottomT{} -> TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTopes TermT n
expected' TermT n
actual'
        TopeEQT{}     -> TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTopes TermT n
expected' TermT n
actual'
        TopeLEQT{}    -> TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTopes TermT n
expected' TermT n
actual'
        TopeAndT{}    -> TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTopes TermT n
expected' TermT n
actual'
        TopeOrT{}     -> TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTopes TermT n
expected' TermT n
actual'
        TopeInvT{}    -> TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTopes TermT n
expected' TermT n
actual'
        TopeUninvT{}  -> TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTopes TermT n
expected' TermT n
actual'

        RecBottomT{} -> () -> TypeCheck n ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- unifies with anything
        RecOrT TypeInfo (TermT n)
_ty [(TermT n, TermT n)]
rs ->
          -- IMPORTANT: matching on actual' here would be redundant, but that is
          -- not obvious; take care when refactoring.
          [(TermT n, TermT n)]
-> ((TermT n, TermT n) -> TypeCheck n ()) -> TypeCheck n ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(TermT n, TermT n)]
rs (((TermT n, TermT n) -> TypeCheck n ()) -> TypeCheck n ())
-> ((TermT n, TermT n) -> TypeCheck n ()) -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ \(TermT n
tope, TermT n
term) ->
            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
term TermT n
actual'

        TypeFunT TypeInfo (TermT n)
_ty Binder
_orig TModality
md TermT n
cube Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret ->
          case TermT n
actual' of
            TypeFunT TypeInfo (TermT n)
_ty' Binder
orig' TModality
md' TermT n
cube' Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope' ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret' -> 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 (String -> TypeError n
forall (n :: S). String -> TypeError n
TypeErrorOther (String -> TypeError n) -> String -> TypeError n
forall a b. (a -> b) -> a -> b
$ String
"modality mismatch in function type: expected " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TModality -> String
forall a. Show a => a -> String
show TModality
md String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" but got " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TModality -> String
forall a. Show a => a -> String
show TModality
md')
              TypeCheck n () -> TypeCheck n ()
forall (n :: S) a. TypeCheck n a -> TypeCheck n a
switchVariance (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$  -- unifying in the negative position!
                TermT n -> TermT n -> TypeCheck n ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTerms TermT n
cube TermT n
cube' -- FIXME: unifyCubes
              Binder
-> TModality
-> TermT n
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TermT l -> TermT l -> TypeCheck l ())
-> TypeCheck n ()
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> ScopedTermT n
-> ScopedTermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TermT l -> TermT l -> TypeCheck l a)
-> TypeCheck n a
inScope2 Binder
orig' TModality
md TermT n
cube' ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret' ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> TermT l -> TermT l -> TypeCheck l ())
 -> TypeCheck n ())
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TermT l -> TermT l -> TypeCheck l ())
-> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder TermT l
retBody TermT l
retBody' -> do
                scope <- (Context l -> Scope l)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Scope l)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context l -> Scope l
forall (n :: S). Context n -> Scope n
ctxScope
                let openTope = (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n -> TermT l)
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> Maybe (TermT l)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Scope l
-> Name l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT 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
binder))
                    mtopeIn = Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> Maybe (TermT l)
openTope Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope
                    mtopeIn' = Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> Maybe (TermT l)
openTope Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope'
                case retBody' of
                  UniverseTopeT{} -> do
                    -- This is the case for tope families (shapes).
                    --
                    -- (Λ → TOPE) <: (Δ → TOPE) since if φ : Λ → TOPE then φ ⊢ Δ.
                    -- We DO NOT take the tope context Φ into account!
                    expectedTopeNF <- TermT l -> Maybe (TermT l) -> TermT l
forall a. a -> Maybe a -> a
fromMaybe TermT l
forall (n :: S). TermT n
topeTopT (Maybe (TermT l) -> TermT l)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TermT l
 -> ReaderT
      (Context l)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (TermT l))
-> Maybe (TermT l)
-> 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 TermT l
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT l)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
nfT Maybe (TermT l)
mtopeIn
                    actualTopeNF   <- fromMaybe topeTopT <$> traverse nfT mtopeIn'
                    let superEntailedBySub TermT n
superNF TermT n
subNF = do
                          entails <- [TermT n -> ModalTope n
forall (n :: S). TermT n -> ModalTope n
plainTope TermT n
subNF] [ModalTope n] -> TermT n -> TypeCheck n Bool
forall (n :: S).
Distinct n =>
[ModalTope n] -> TermT n -> TypeCheck n Bool
`entailM` TermT n
superNF
                          unless (entails || containsHole subNF || containsHole superNF) $
                            issueTypeError (TypeErrorTopeNotSatisfied [subNF] superNF)
                    bySubtyping superEntailedBySub expectedTopeNF actualTopeNF
                  TermT l
_ -> do
                    -- this is the case for Π-types and extension types
                    --
                    -- Ξ | Φ | Γ ⊢ {t : I | φ} → A t <: {s : J | ψ} → B s
                    -- when Ξ | Φ, ψ ⊢ φ
                    expectedTopeNF <- TermT l -> Maybe (TermT l) -> TermT l
forall a. a -> Maybe a -> a
fromMaybe TermT l
forall (n :: S). TermT n
topeTopT (Maybe (TermT l) -> TermT l)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT l))
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TermT l
 -> ReaderT
      (Context l)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (TermT l))
-> Maybe (TermT l)
-> 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 TermT l
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT l)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
nfT Maybe (TermT l)
mtopeIn
                    actualTopeNF   <- fromMaybe topeTopT <$> traverse nfT mtopeIn'
                    bySubtyping domainEntails expectedTopeNF actualTopeNF
                case mterm of
                  Maybe (TermT n)
Nothing -> TermT l -> TermT l -> TypeCheck l ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
unifyTerms TermT l
retBody TermT l
retBody'
                  Just TermT n
term ->
                    TermT l -> TermT l -> TermT l -> TypeCheck l ()
forall (n :: S).
Distinct n =>
TermT n -> TermT n -> TermT n -> TypeCheck n ()
unifyTypes
                      (TermT l -> TermT l -> TermT l -> TermT l
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT TermT l
retBody' (TermT n -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
term) (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)))
                      TermT l
retBody TermT l
retBody'
            TermT n
_ -> TypeCheck n ()
err

        TypeSigmaT TypeInfo (TermT n)
_ty Binder
_orig TModality
md TermT n
a ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
b ->
          case TermT n
actual' of
            TypeSigmaT TypeInfo (TermT n)
_ty' Binder
orig' TModality
md' TermT n
a' ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
b' -> 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 (String -> TypeError n
forall (n :: S). String -> TypeError n
TypeErrorOther (String -> TypeError n) -> String -> TypeError n
forall a b. (a -> b) -> a -> b
$ String
"modality mismatch in sigma type: expected " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TModality -> String
forall a. Show a => a -> String
show TModality
md String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" but got " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TModality -> String
forall a. Show a => a -> String
show TModality
md')
              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
a'
              Binder
-> TModality
-> TermT n
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TermT l -> TermT l -> TypeCheck l ())
-> TypeCheck n ()
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> ScopedTermT n
-> ScopedTermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TermT l -> TermT l -> TypeCheck l a)
-> TypeCheck n a
inScope2 Binder
orig' TModality
md TermT n
a' ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
b ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
b' ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> TermT l -> TermT l -> TypeCheck l ())
 -> TypeCheck n ())
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TermT l -> TermT l -> TypeCheck l ())
-> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
_binder TermT l
bBody TermT l
bBody' ->
                Maybe (TermT l) -> TermT l -> TermT l -> TypeCheck l ()
forall (n :: S).
Distinct n =>
Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
unify Maybe (TermT l)
forall a. Maybe a
Nothing TermT l
bBody TermT l
bBody'
            TermT n
_ -> TypeCheck n ()
err

        TypeIdT TypeInfo (TermT n)
_ty TermT n
x Maybe (TermT n)
tA TermT n
y ->
          case TermT n
actual' of
            TypeIdT TypeInfo (TermT n)
_ty' TermT n
x' Maybe (TermT n)
tA' TermT n
y' -> do
              -- The underlying types must be compared: without this check the
              -- routine equates identity types over different types whenever the
              -- endpoints unify, accepting a free homotopy (a path in the type of
              -- functions) where an endpoint-fixing one (a path in a hom-type) is
              -- expected. Compared invariantly: subtyping between the underlying
              -- types must not leak into equality of identity types over them.
              ((TermT n, TermT n) -> TypeCheck n ())
-> Maybe (TermT n, TermT n) -> TypeCheck n ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(TermT n
t1, TermT n
t2) -> Covariance -> TypeCheck n () -> TypeCheck n ()
forall (n :: S) a. Covariance -> TypeCheck n a -> TypeCheck n a
setVariance Covariance
Invariant (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
t1 TermT n
t2))
                ((,) (TermT n -> TermT n -> (TermT n, TermT n))
-> Maybe (TermT n) -> Maybe (TermT n -> (TermT n, TermT n))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (TermT n)
tA Maybe (TermT n -> (TermT n, TermT n))
-> Maybe (TermT n) -> Maybe (TermT n, TermT n)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe (TermT n)
tA')
              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
x TermT n
x'
              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
y TermT n
y'
            TermT n
_ -> TypeCheck n ()
err

        AppT TypeInfo (TermT n)
_ty TermT n
f TermT n
x ->
          case TermT n
actual' of
            AppT TypeInfo (TermT n)
_ty' TermT n
f' TermT n
x' -> do
              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
f TermT n
f'
              Covariance -> TypeCheck n () -> TypeCheck n ()
forall (n :: S) a. Covariance -> TypeCheck n a -> TypeCheck n a
setVariance Covariance
Invariant (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$
                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
x TermT n
x'
            TermT n
_ -> TypeCheck n ()
err

        LambdaT TypeInfo (TermT n)
ty Binder
_orig Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
_mparam ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
body ->
          case TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
stripTypeRestrictions (TypeInfo (TermT n) -> TermT n
forall term. TypeInfo term -> term
infoType TypeInfo (TermT n)
ty) of
            TypeFunT TypeInfo (TermT n)
_ty Binder
_origF TModality
md TermT n
param Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
_ret ->
              case TermT n
actual' of
                LambdaT TypeInfo (TermT n)
ty' Binder
orig' Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
_mparam' ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
body' ->
                  case TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
stripTypeRestrictions (TypeInfo (TermT n) -> TermT n
forall term. TypeInfo term -> term
infoType TypeInfo (TermT n)
ty') of
                    TypeFunT TypeInfo (TermT n)
_ty' Binder
_origF' TModality
md' TermT n
param' Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope' ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
_ret' -> 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 (String -> TypeError n
forall (n :: S). String -> TypeError n
TypeErrorOther (String -> TypeError n) -> String -> TypeError n
forall a b. (a -> b) -> a -> b
$ String
"modality mismatch in lambda: expected " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TModality -> String
forall a. Show a => a -> String
show TModality
md String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" but got " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TModality -> String
forall a. Show a => a -> String
show TModality
md')
                      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
param TermT n
param' -- we (should) have already checked this in types!
                      Binder
-> TModality
-> TermT n
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TermT l -> TermT l -> TypeCheck l ())
-> TypeCheck n ()
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> ScopedTermT n
-> ScopedTermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TermT l -> TermT l -> TypeCheck l a)
-> TypeCheck n a
inScope2 Binder
orig' TModality
md TermT n
param ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
body ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
body' ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> TermT l -> TermT l -> TypeCheck l ())
 -> TypeCheck n ())
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TermT l -> TermT l -> TypeCheck l ())
-> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder TermT l
bodyIn TermT l
bodyIn' -> do
                        scope <- (Context l -> Scope l)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Scope l)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context l -> Scope l
forall (n :: S). Context n -> Scope n
ctxScope
                        let openTope = (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n -> TermT l)
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> Maybe (TermT l)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Scope l
-> Name l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT 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
binder))
                        case (openTope mtope, openTope mtope') of
                          (Just TermT l
tope, Just TermT l
tope') -> do
                            -- The two lambdas need not stand on the same shape.
                            -- η-expansion takes the domain tope from the
                            -- function's own type, so this is the same
                            -- obligation as for the Π-type above.
                            (TermT l -> TermT l -> TypeCheck l ())
-> TermT l -> TermT l -> TypeCheck l ()
forall (n :: S).
(TermT n -> TermT n -> TypeCheck n ())
-> TermT n -> TermT n -> TypeCheck n ()
bySubtyping TermT l -> TermT l -> TypeCheck l ()
forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
domainEntails TermT l
tope TermT l
tope'
                            -- The bodies agree only where both are defined.
                            TermT l -> TypeCheck l () -> TypeCheck l ()
forall (n :: S) a.
Distinct n =>
TermT n -> TypeCheck n a -> TypeCheck n a
localTope (TermT l -> TermT l -> TermT l
forall (n :: S). TermT n -> TermT n -> TermT n
topeAndT TermT l
tope TermT l
tope') (TypeCheck l () -> TypeCheck l ())
-> TypeCheck l () -> TypeCheck l ()
forall a b. (a -> b) -> a -> b
$
                              Maybe (TermT l) -> TermT l -> TermT l -> TypeCheck l ()
forall (n :: S).
Distinct n =>
Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
unify Maybe (TermT l)
forall a. Maybe a
Nothing TermT l
bodyIn TermT l
bodyIn'
                          (Maybe (TermT l)
Nothing, Maybe (TermT l)
Nothing) ->
                            Maybe (TermT l) -> TermT l -> TermT l -> TypeCheck l ()
forall (n :: S).
Distinct n =>
Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
unify Maybe (TermT l)
forall a. Maybe a
Nothing TermT l
bodyIn TermT l
bodyIn'
                          (Maybe (TermT l), Maybe (TermT l))
_ -> TypeCheck l ()
forall (l :: S). DExt n l => TypeCheck l ()
errIn
                    TermT n
_ -> TypeCheck n ()
err
                TermT n
_ -> TypeCheck n ()
err
            TermT n
_ -> TypeCheck n ()
err

        LetT{} -> String -> TypeCheck n ()
forall a. String -> a
panicImpossible String
"let at the root of WHNF"
        -- The bind annotation and the motive are both elaboration annotations: they
        -- fix how the let is typed, but they do not contribute to its value. Two
        -- stuck @let mod@s with the same modalities, value, and body are therefore
        -- the same term whichever motive each was written with, so neither
        -- annotation is compared here.
        LetModT TypeInfo (TermT n)
_ Binder
orig TModality
app TModality
inn Maybe (TermT n)
_ Maybe (TermT n)
_mmotive TermT n
val ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
body ->
          case TermT n
actual' of
            LetModT TypeInfo (TermT n)
_ Binder
_ TModality
app' TModality
inn' Maybe (TermT n)
_ Maybe (TermT n)
_mmotive' TermT n
val' ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
body'
              | TModality
app TModality -> TModality -> Bool
forall a. Eq a => a -> a -> Bool
== TModality
app', TModality
inn TModality -> TModality -> Bool
forall a. Eq a => a -> a -> Bool
== TModality
inn' -> do
                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
val TermT n
val'
                bty <- TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
val 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
                  TypeModalT TypeInfo (TermT n)
_ TModality
_ 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
                  TermT n
_ -> String -> TypeCheck n (TermT n)
forall a. String -> a
panicImpossible String
"not modal in letmod"
                inScope2 orig (comp app inn) bty body body' $ \NameBinder n l
_binder TermT l
bodyIn TermT l
bodyIn' ->
                  Maybe (TermT l) -> TermT l -> TermT l -> TypeCheck l ()
forall (n :: S).
Distinct n =>
Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
unify Maybe (TermT l)
forall a. Maybe a
Nothing TermT l
bodyIn TermT l
bodyIn'
            TermT n
_ -> TypeCheck n ()
err

        ReflT TypeInfo (TermT n)
ty Maybe (TermT n, Maybe (TermT n))
_x | TypeIdT TypeInfo (TermT n)
_ty TermT n
x Maybe (TermT n)
_tA TermT n
y <- TypeInfo (TermT n) -> TermT n
forall term. TypeInfo term -> term
infoType TypeInfo (TermT n)
ty ->
          case TermT n
actual' of
            ReflT TypeInfo (TermT n)
ty' Maybe (TermT n, Maybe (TermT n))
_x' | TypeIdT TypeInfo (TermT n)
_ty' TermT n
x' Maybe (TermT n)
_tA' TermT n
y' <- TypeInfo (TermT n) -> TermT n
forall term. TypeInfo term -> term
infoType TypeInfo (TermT n)
ty' -> do
              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
x TermT n
x'
              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
y TermT n
y'
            TermT n
_ -> TypeCheck n ()
err
        ReflT{} -> String -> TypeCheck n ()
forall a. String -> a
panicImpossible String
"refl with a non-identity type!"

        IdJT TypeInfo (TermT n)
_ty TermT n
a TermT n
b TermT n
c TermT n
d TermT n
e TermT n
f ->
          case TermT n
actual' of
            IdJT TypeInfo (TermT n)
_ty' TermT n
a' TermT n
b' TermT n
c' TermT n
d' TermT n
e' TermT n
f' -> do
              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
a'
              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
b TermT n
b'
              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
c TermT n
c'
              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
d TermT n
d'
              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
e TermT n
e'
              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
f TermT n
f'
            TermT n
_ -> TypeCheck n ()
err

        TypeAscT{} -> String -> TypeCheck n ()
forall a. String -> a
panicImpossible String
"type ascription at the root of WHNF"

        TypeRestrictedT TypeInfo (TermT n)
_ty TermT n
ty [(TermT n, TermT n)]
rs ->
          case TermT n
actual' of
            TypeRestrictedT TypeInfo (TermT n)
_ty' TermT n
ty' [(TermT n, TermT n)]
rs' -> do
              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)
mterm TermT n
ty TermT n
ty'
              -- The faces of the supertype must be covered by the faces of the
              -- subtype (the subtype is at least as specified), with the boundary
              -- terms agreeing on overlaps. Which side is the subtype depends on the
              -- ambient variance.
              variance <- (Context n -> Covariance)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Covariance
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context n -> Covariance
forall (n :: S). Context n -> Covariance
ctxCovariance
              let subCoversSuper [(TermT n, TermT n)]
subRs [(TermT n, TermT n)]
superRs = [ReaderT
   (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()]
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_
                    [ TermT n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S) a.
Distinct n =>
TermT n -> TypeCheck n a -> TypeCheck n a
localTope TermT n
tope (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
                        -- FIXME: can do less entails checks?
                        TermT n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S). Distinct n => TermT n -> TypeCheck n ()
contextEntails ((TermT n -> TermT n -> TermT n) -> TermT n -> [TermT n] -> TermT n
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeOrT TermT n
forall (n :: S). TermT n
topeBottomT (((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)]
subRs))
                        [(TermT n, TermT n)]
-> ((TermT n, TermT 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_ [(TermT n, TermT n)]
subRs (((TermT n, TermT n)
  -> ReaderT
       (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> ((TermT n, TermT n)
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ())
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall a b. (a -> b) -> a -> b
$ \(TermT n
tope', TermT n
term') ->
                          TermT n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
forall (n :: S) a.
Distinct n =>
TermT n -> TypeCheck n a -> TypeCheck n a
localTope TermT n
tope' (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
$
                            Maybe (TermT n)
-> TermT n
-> TermT n
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
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
term TermT n
term'
                    | (TermT n
tope, TermT n
term) <- [(TermT n, TermT n)]
superRs
                    ]
              case variance of
                Covariance
Covariant     -> [(TermT n, TermT n)] -> [(TermT n, TermT n)] -> TypeCheck n ()
forall {n :: S}.
Distinct n =>
[(TermT n, TermT n)]
-> [(TermT n, TermT n)]
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
subCoversSuper [(TermT n, TermT n)]
rs' [(TermT n, TermT n)]
rs
                Covariance
Contravariant -> [(TermT n, TermT n)] -> [(TermT n, TermT n)] -> TypeCheck n ()
forall {n :: S}.
Distinct n =>
[(TermT n, TermT n)]
-> [(TermT n, TermT n)]
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
subCoversSuper [(TermT n, TermT n)]
rs [(TermT n, TermT n)]
rs'
                Covariance
Invariant     -> do
                  [(TermT n, TermT n)] -> [(TermT n, TermT n)] -> TypeCheck n ()
forall {n :: S}.
Distinct n =>
[(TermT n, TermT n)]
-> [(TermT n, TermT n)]
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
subCoversSuper [(TermT n, TermT n)]
rs' [(TermT n, TermT n)]
rs
                  [(TermT n, TermT n)] -> [(TermT n, TermT n)] -> TypeCheck n ()
forall {n :: S}.
Distinct n =>
[(TermT n, TermT n)]
-> [(TermT n, TermT n)]
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) ()
subCoversSuper [(TermT n, TermT n)]
rs [(TermT n, TermT n)]
rs'
            TermT n
_ -> TypeCheck n ()
err    -- FIXME: need better unification for restrictions

        TypeModalT TypeInfo (TermT n)
_ty TModality
m TermT n
ty ->
          case TermT n
actual' of
            TypeModalT TypeInfo (TermT n)
_ty' TModality
m' TermT n
ty' -> do
              Bool -> TypeCheck n () -> TypeCheck n ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TModality
m' TModality -> TModality -> Bool
forall a. Eq a => a -> a -> Bool
/= TModality
m) TypeCheck n ()
err
              TModality -> TypeCheck n () -> TypeCheck n ()
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
m (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ 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
ty TermT n
ty'
            TermT n
_ -> TypeCheck n ()
err
        ModAppT TypeInfo (TermT n)
_ty TModality
m TermT n
ty ->
          case TermT n
actual' of
            ModAppT TypeInfo (TermT n)
_ty' TModality
m' TermT n
ty' -> do
              Bool -> TypeCheck n () -> TypeCheck n ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TModality
m' TModality -> TModality -> Bool
forall a. Eq a => a -> a -> Bool
/= TModality
m) TypeCheck n ()
err
              TModality -> TypeCheck n () -> TypeCheck n ()
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
m (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ 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
ty TermT n
ty'
            TermT n
_ -> TypeCheck n ()
err
        -- The external component of an extraction is bookkeeping, not
        -- denotation: it records the lock under which the extracted value was
        -- checked, so that evaluation re-enters it correctly, but the term
        -- denotes the counit of the inner modality at the value either way.
        -- It is also not canonical: 'etaExpand' always writes @Id@, while the
        -- elaboration of @let ν mod µ@ writes ν, so comparing the external
        -- components would sever η-equal spellings of the same counit
        -- (e.g. @$extract$ ♯/♯ t@ against @$extract$ _id/♯ t@).
        ModExtractT TypeInfo (TermT n)
_ty TModality
app TModality
inn TermT n
te ->
          case TermT n
actual' of
            ModExtractT TypeInfo (TermT n)
_ty' TModality
_app' TModality
inn' TermT n
te' -> do
              Bool -> TypeCheck n () -> TypeCheck n ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TModality
inn' TModality -> TModality -> Bool
forall a. Eq a => a -> a -> Bool
/= TModality
inn) TypeCheck n ()
err
              TModality -> TypeCheck n () -> TypeCheck n ()
forall (n :: S) b.
Distinct n =>
TModality -> TypeCheck n b -> TypeCheck n b
enterModality TModality
app (TypeCheck n () -> TypeCheck n ())
-> TypeCheck n () -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ 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
te TermT n
te'
            TermT n
_ -> TypeCheck n ()
err

        -- defensive: a hole nested anywhere also defers here rather than panicking
        -- on an otherwise unexpected shape
        TermT n
_ | Bool
holePresent -> () -> TypeCheck n ()
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        TermT n
_ -> String -> TypeCheck n ()
forall a. String -> a
panicImpossible String
"unexpected term in UNIFY"