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

-- | The elaborated types of a declaration's local binders, for LSP hover.
--
-- Every node of a typed term carries its type, so even a bare λ's binder is typed
-- — by the domain of the λ's own Π-type.
--
-- The old version threaded a @BinderNames@ environment down through the term, to
-- say what each variable it met was called. There is no need: entering a binder
-- puts it in the context, and the context already knows what everything in it is
-- called (see "Rzk.TypeCheck.Display").
module Rzk.TypeCheck.BinderTypes where

import           Control.Monad.Except     (catchError)
import           Control.Monad.Reader     (asks)
import           Data.Bifoldable          (bifoldr)
import           Data.Maybe               (fromMaybe)

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

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

-- | A binder's displayed type: a plain type, or a cube together with a tope, for a
-- shaped binder like @(t : I | φ t)@.
data BinderTypeView
  = TypeView Rendered
  | ShapeView Rendered Rendered
  deriving (BinderTypeView -> BinderTypeView -> Bool
(BinderTypeView -> BinderTypeView -> Bool)
-> (BinderTypeView -> BinderTypeView -> Bool) -> Eq BinderTypeView
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BinderTypeView -> BinderTypeView -> Bool
== :: BinderTypeView -> BinderTypeView -> Bool
$c/= :: BinderTypeView -> BinderTypeView -> Bool
/= :: BinderTypeView -> BinderTypeView -> Bool
Eq, Int -> BinderTypeView -> ShowS
[BinderTypeView] -> ShowS
BinderTypeView -> String
(Int -> BinderTypeView -> ShowS)
-> (BinderTypeView -> String)
-> ([BinderTypeView] -> ShowS)
-> Show BinderTypeView
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BinderTypeView -> ShowS
showsPrec :: Int -> BinderTypeView -> ShowS
$cshow :: BinderTypeView -> String
show :: BinderTypeView -> String
$cshowList :: [BinderTypeView] -> ShowS
showList :: [BinderTypeView] -> ShowS
Show)

-- | Render a term with the names of the context it is in.
renderHere :: TermT n -> TypeCheck n Rendered
renderHere :: forall (n :: S). TermT n -> TypeCheck n Rendered
renderHere TermT n
t = do
  naming <- (Context n -> Naming n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Naming n)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context n -> Naming n
forall (n :: S). Context n -> Naming n
namingOfContext
  pure (renderTerm naming (untyped t))

-- | The memoised weak head normal form of a typed term, if present.
memoWHNF :: TermT n -> TermT n
memoWHNF :: forall (n :: S). TermT n -> TermT n
memoWHNF TermT n
t = TermT n -> Maybe (TermT n) -> TermT n
forall a. a -> Maybe a -> a
fromMaybe TermT n
t (TermT n -> Maybe (TypeInfo (TermT n))
forall (n :: S). TermT n -> Maybe (TypeInfo (TermT n))
typeInfoOf TermT n
t Maybe (TypeInfo (TermT n))
-> (TypeInfo (TermT n) -> Maybe (TermT n)) -> Maybe (TermT n)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TypeInfo (TermT n) -> Maybe (TermT n)
forall term. TypeInfo term -> Maybe term
infoWHNF)

-- | The variables a binder introduces, with their rendered types.
--
-- A pair binder splits its type along Σ-types and cube products; when the shape is
-- not syntactic (the type is a defined name applied to arguments, as in
-- @((η , (ϵ , (α , β))) : has-quasi-diagrammatic-adj A B f u)@), the type is put in
-- weak head normal form first, which needs the top-level definitions in scope. The
-- dependent part is rendered under the earlier component's display name, giving
-- @q : B p@.
binderTypeEntries
  :: Distinct n => Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
binderTypeEntries :: forall (n :: S).
Distinct n =>
Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
binderTypeEntries Binder
binder TermT n
ty = case Binder
binder of
  Binder
BinderUnit         -> [(VarIdent, BinderTypeView)]
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  BinderVar Maybe VarIdent
Nothing  -> [(VarIdent, BinderTypeView)]
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  BinderVar (Just VarIdent
x) -> do
    rendered <- TermT n -> TypeCheck n Rendered
forall (n :: S). TermT n -> TypeCheck n Rendered
renderHere TermT n
ty
    pure [(x, TypeView rendered)]
  BinderPair Binder
l Binder
r     -> TermT n -> TypeCheck n (Maybe (TermT n))
forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n (Maybe (TermT n))
splitViewM TermT n
ty TypeCheck n (Maybe (TermT n))
-> (Maybe (TermT n) -> TypeCheck n [(VarIdent, BinderTypeView)])
-> TypeCheck n [(VarIdent, BinderTypeView)]
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
    Just (TypeSigmaT TypeInfo (TermT n)
_ Binder
_ TModality
md TermT n
a ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
bscope) -> do
      ls <- Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
binderTypeEntries Binder
l TermT n
a
      rs <- inScope l md a bscope $ \AST NameBinder (AnnSig TypeInfo TermSig) l
bBody -> Binder
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> TypeCheck l [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
binderTypeEntries Binder
r AST NameBinder (AnnSig TypeInfo TermSig) l
bBody
      pure (ls ++ rs)
    Just (CubeProductT TypeInfo (TermT n)
_ TermT n
a TermT n
b) ->
      [(VarIdent, BinderTypeView)]
-> [(VarIdent, BinderTypeView)] -> [(VarIdent, BinderTypeView)]
forall a. [a] -> [a] -> [a]
(++) ([(VarIdent, BinderTypeView)]
 -> [(VarIdent, BinderTypeView)] -> [(VarIdent, BinderTypeView)])
-> TypeCheck n [(VarIdent, BinderTypeView)]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     ([(VarIdent, BinderTypeView)] -> [(VarIdent, BinderTypeView)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
binderTypeEntries Binder
l TermT n
a ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  ([(VarIdent, BinderTypeView)] -> [(VarIdent, BinderTypeView)])
-> TypeCheck n [(VarIdent, BinderTypeView)]
-> TypeCheck n [(VarIdent, BinderTypeView)]
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
<*> Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
binderTypeEntries Binder
r TermT n
b
    Maybe (TermT n)
_ -> [(VarIdent, BinderTypeView)]
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []   -- unrecognised shape; the surface annotation is the fallback

-- | View a type as a Σ-type or a cube product: syntactically, or through the
-- memoised WHNF if possible, computing the WHNF otherwise. Never throws.
splitViewM :: Distinct n => TermT n -> TypeCheck n (Maybe (TermT n))
splitViewM :: forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n (Maybe (TermT n))
splitViewM TermT n
ty = case TermT n -> Maybe (TermT n)
forall {n :: S}. TermT n -> Maybe (TermT n)
splitView (TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
memoWHNF TermT n
ty) of
  Just TermT n
t  -> Maybe (TermT n) -> TypeCheck n (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
t)
  Maybe (TermT n)
Nothing -> (TermT n -> Maybe (TermT n)
forall {n :: S}. TermT n -> Maybe (TermT n)
splitView (TermT n -> Maybe (TermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
-> TypeCheck n (Maybe (TermT n))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TermT n
ty) TypeCheck n (Maybe (TermT n))
-> (TypeErrorInScopedContext -> TypeCheck n (Maybe (TermT n)))
-> TypeCheck n (Maybe (TermT 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
_ -> Maybe (TermT n) -> TypeCheck n (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (TermT n)
forall a. Maybe a
Nothing
  where
    splitView :: TermT n -> Maybe (TermT n)
splitView TermT n
t = case TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
stripTypeRestrictions TermT n
t of
      t' :: TermT n
t'@TypeSigmaT{}   -> TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
t'
      t' :: TermT n
t'@CubeProductT{} -> TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
t'
      TermT n
_                 -> Maybe (TermT n)
forall a. Maybe a
Nothing

-- | The elaborated types of the local binders of a typed term, keyed by the
-- binder's original identifier (whose position points at its defining occurrence).
binderTypesOfTerm
  :: Distinct n => TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
binderTypesOfTerm :: forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
binderTypesOfTerm = TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
go
  where
    go :: Distinct n => TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
    go :: forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
go TermT n
t = case TermT n
t of
      Var Name n
_ -> [(VarIdent, BinderTypeView)]
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

      LambdaT TypeInfo (TermT n)
info Binder
binder Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
mparam ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
body -> do
        (paramType, paramTope) <- case Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
mparam of
          Just (LambdaParam TModality
_ TermT n
ty Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope) -> (Maybe (TermT n),
 Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n),
      Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
ty, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope)
          -- A bare λ: the domain (and shape) of its own Π-type.
          Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
Nothing -> case TermT n
-> Maybe
     (TermT n, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
forall {n :: S}.
TermT n
-> Maybe
     (TermT n, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
funView (TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
memoWHNF (TypeInfo (TermT n) -> TermT n
forall term. TypeInfo term -> term
infoType TypeInfo (TermT n)
info)) of
            Just (TermT n
p, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope) -> (Maybe (TermT n),
 Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n),
      Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
p, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope)
            Maybe
  (TermT n, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
Nothing ->
              ((Maybe (TermT n),
 Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
-> ((TermT n,
     Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
    -> (Maybe (TermT n),
        Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)))
-> Maybe
     (TermT n, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
-> (Maybe (TermT n),
    Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Maybe (TermT n)
forall a. Maybe a
Nothing, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. Maybe a
Nothing) (\(TermT n
p, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope) -> (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
p, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope)) (Maybe
   (TermT n, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
 -> (Maybe (TermT n),
     Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)))
-> (TermT n
    -> Maybe
         (TermT n,
          Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)))
-> TermT n
-> (Maybe (TermT n),
    Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermT n
-> Maybe
     (TermT n, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
forall {n :: S}.
TermT n
-> Maybe
     (TermT n, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
funView
                 (TermT n
 -> (Maybe (TermT n),
     Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n),
      Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT (TypeInfo (TermT n) -> TermT n
forall term. TypeInfo term -> term
infoType TypeInfo (TermT n)
info))
                ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Maybe (TermT n),
   Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe (TermT n),
          Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n),
      Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) 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
_ -> (Maybe (TermT n),
 Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n),
      Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (TermT n)
forall a. Maybe a
Nothing, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. Maybe a
Nothing)
        entries <- shapedBinderEntries binder paramType paramTope
        let md = TModality
-> (LambdaParam
      (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n)
    -> TModality)
-> Maybe
     (LambdaParam
        (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
-> TModality
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TModality
Id (\(LambdaParam TModality
m TermT n
_ Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_) -> TModality
m) Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
mparam
        annEntries <- case mparam of
          Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
Nothing -> [(VarIdent, BinderTypeView)]
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
          Just (LambdaParam TModality
_ TermT n
ty Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope) -> do
            tyEntries <- TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
go TermT n
ty
            topeEntries <- case mtope of
              Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
Nothing   -> [(VarIdent, BinderTypeView)]
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
              Just ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
tope -> Binder
-> TModality
-> TermT n
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    AST NameBinder (AnnSig TypeInfo TermSig) l
    -> TypeCheck l [(VarIdent, BinderTypeView)])
-> TypeCheck n [(VarIdent, BinderTypeView)]
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
binder TModality
md TermT n
ty ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
tope TermT l -> TypeCheck l [(VarIdent, BinderTypeView)]
forall (l :: S).
(DExt n l, Distinct l) =>
AST NameBinder (AnnSig TypeInfo TermSig) l
-> TypeCheck l [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
go
            pure (tyEntries ++ topeEntries)
        bodyEntries <-
          inScope binder md (fromMaybe universeT paramType) body go
        pure (entries ++ annEntries ++ bodyEntries)

      TypeFunT TypeInfo (TermT n)
_ Binder
binder TModality
md TermT n
param Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret -> do
        entries      <- Binder
-> Maybe (TermT n)
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
Binder
-> Maybe (TermT n)
-> Maybe (ScopedTermT n)
-> TypeCheck n [(VarIdent, BinderTypeView)]
shapedBinderEntries Binder
binder (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
param) Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope
        paramEntries <- go param
        topeEntries  <- case mtope of
          Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
Nothing   -> [(VarIdent, BinderTypeView)]
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
          Just ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
tope -> Binder
-> TModality
-> TermT n
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    AST NameBinder (AnnSig TypeInfo TermSig) l
    -> TypeCheck l [(VarIdent, BinderTypeView)])
-> TypeCheck n [(VarIdent, BinderTypeView)]
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
binder TModality
md TermT n
param ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
tope TermT l -> TypeCheck l [(VarIdent, BinderTypeView)]
forall (l :: S).
(DExt n l, Distinct l) =>
AST NameBinder (AnnSig TypeInfo TermSig) l
-> TypeCheck l [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
go
        retEntries   <- inScope binder md param ret go
        pure (entries ++ paramEntries ++ topeEntries ++ retEntries)

      TypeSigmaT TypeInfo (TermT n)
_ Binder
binder TModality
md TermT n
a ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
bscope -> do
        entries  <- Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
binderTypeEntries Binder
binder TermT n
a
        aEntries <- go a
        bEntries <- inScope binder md a bscope go
        pure (entries ++ aEntries ++ bEntries)

      LetT TypeInfo (TermT n)
_ Binder
binder Maybe (TermT n)
manno TermT n
value ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
body -> do
        let valueType :: Maybe (TermT n)
valueType = case TermT n -> Maybe (TypeInfo (TermT n))
forall (n :: S). TermT n -> Maybe (TypeInfo (TermT n))
typeInfoOf TermT n
value of
              Just TypeInfo (TermT n)
valueInfo -> TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just (TypeInfo (TermT n) -> TermT n
forall term. TypeInfo term -> term
infoType TypeInfo (TermT n)
valueInfo)
              Maybe (TypeInfo (TermT n))
Nothing        -> Maybe (TermT n)
manno
        entries      <- TypeCheck n [(VarIdent, BinderTypeView)]
-> (TermT n -> TypeCheck n [(VarIdent, BinderTypeView)])
-> Maybe (TermT n)
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([(VarIdent, BinderTypeView)]
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []) (Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
binderTypeEntries Binder
binder) Maybe (TermT n)
valueType
        annEntries   <- maybe (pure []) go manno
        valueEntries <- go value
        bodyEntries  <- inScopeWith binder Id (fromMaybe universeT valueType) (Just value) body go
        pure (entries ++ annEntries ++ valueEntries ++ bodyEntries)

      LetModT TypeInfo (TermT n)
_ Binder
binder TModality
_nu TModality
mu Maybe (TermT n)
manno Maybe (TermT n)
mmotive TermT n
value ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
body -> do
        unwrapped <- case TermT n -> Maybe (TypeInfo (TermT n))
forall (n :: S). TermT n -> Maybe (TypeInfo (TermT n))
typeInfoOf TermT n
value of
          Maybe (TypeInfo (TermT n))
Nothing -> Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (TermT n)
forall a. Maybe a
Nothing
          Just TypeInfo (TermT n)
valueInfo -> do
            let vt :: TermT n
vt = TypeInfo (TermT n) -> TermT n
forall term. TypeInfo term -> term
infoType TypeInfo (TermT n)
valueInfo
            case TermT n -> Maybe (TermT n)
forall {n :: S}. TermT n -> Maybe (TermT n)
modalView (TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
memoWHNF TermT n
vt) of
              Just TermT n
a  -> Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
a)
              Maybe (TermT n)
Nothing -> (TermT n -> Maybe (TermT n)
forall {n :: S}. TermT n -> Maybe (TermT n)
modalView (TermT n -> Maybe (TermT n))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TermT n
vt) ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  (Maybe (TermT n))
-> (TypeErrorInScopedContext
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe (TermT n)))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT 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
_ -> Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (TermT n))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (TermT n)
forall a. Maybe a
Nothing
        entries      <- maybe (pure []) (binderTypeEntries binder) unwrapped
        annEntries   <- maybe (pure []) go manno
        motiveEntries <- maybe (pure []) go mmotive
        valueEntries <- go value
        bodyEntries  <- inScope binder mu (fromMaybe universeT unwrapped) body go
        pure (entries ++ annEntries ++ motiveEntries ++ valueEntries ++ bodyEntries)

      Node (AnnSig TypeInfo (TermT n)
_ TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n)
f) ->
        [[(VarIdent, BinderTypeView)]] -> [(VarIdent, BinderTypeView)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(VarIdent, BinderTypeView)]] -> [(VarIdent, BinderTypeView)])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [[(VarIdent, BinderTypeView)]]
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TermT n -> TypeCheck n [(VarIdent, BinderTypeView)])
-> [TermT n]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [[(VarIdent, BinderTypeView)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
go ((ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
 -> [TermT n] -> [TermT n])
-> (TermT n -> [TermT n] -> [TermT n])
-> [TermT n]
-> TermSig
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n)
-> [TermT n]
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) n
_ [TermT n]
acc -> [TermT n]
acc) (:) [] TermSig
  (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n)
f)

    funView :: TermT n
-> Maybe
     (TermT n, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
funView TermT n
t = case TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
stripTypeRestrictions TermT n
t of
      TypeFunT TypeInfo (TermT n)
_ Binder
_ TModality
_ TermT n
param Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
_ -> (TermT n, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
-> Maybe
     (TermT n, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
forall a. a -> Maybe a
Just (TermT n
param, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope)
      TermT n
_                            -> Maybe
  (TermT n, Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n))
forall a. Maybe a
Nothing
    modalView :: TermT n -> Maybe (TermT n)
modalView TermT n
t = case TermT n -> TermT n
forall (n :: S). TermT n -> TermT n
stripTypeRestrictions TermT n
t of
      TypeModalT TypeInfo (TermT n)
_ TModality
_ TermT n
a -> TermT n -> Maybe (TermT n)
forall a. a -> Maybe a
Just TermT n
a
      TermT n
_                -> Maybe (TermT n)
forall a. Maybe a
Nothing

    -- A shaped plain binder shows its cube together with the tope, as it is
    -- written: (t : I | φ t). A shaped pair binder splits along the cube, the tope
    -- constraining the components jointly (as in the surface tier).
    shapedBinderEntries
      :: Distinct n
      => Binder -> Maybe (TermT n) -> Maybe (ScopedTermT n)
      -> TypeCheck n [(VarIdent, BinderTypeView)]
    shapedBinderEntries :: forall (n :: S).
Distinct n =>
Binder
-> Maybe (TermT n)
-> Maybe (ScopedTermT n)
-> TypeCheck n [(VarIdent, BinderTypeView)]
shapedBinderEntries Binder
binder Maybe (TermT n)
mty Maybe (ScopedTermT n)
mtope = case (Binder
binder, Maybe (TermT n)
mty, Maybe (ScopedTermT n)
mtope) of
      (BinderVar (Just VarIdent
x), Just TermT n
cube, Just ScopedTermT n
tope) -> do
        cubeR <- TermT n -> TypeCheck n Rendered
forall (n :: S). TermT n -> TypeCheck n Rendered
renderHere TermT n
cube
        topeR <- inScope binder Id cube tope renderHere
        pure [(x, ShapeView cubeR topeR)]
      (Binder
_, Just TermT n
ty, Maybe (ScopedTermT n)
_) -> Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
binderTypeEntries Binder
binder TermT n
ty
      (Binder, Maybe (TermT n), Maybe (ScopedTermT n))
_ -> [(VarIdent, BinderTypeView)]
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

-- | All the local binder types of a declaration: Π and Σ binders from its type,
-- λ and let binders from its value.
declBinderTypes
  :: Distinct n => Decl n -> TypeCheck n [(VarIdent, BinderTypeView)]
declBinderTypes :: forall (n :: S).
Distinct n =>
Decl n -> TypeCheck n [(VarIdent, BinderTypeView)]
declBinderTypes Decl n
decl =
  [(VarIdent, BinderTypeView)]
-> [(VarIdent, BinderTypeView)] -> [(VarIdent, BinderTypeView)]
forall a. [a] -> [a] -> [a]
(++) ([(VarIdent, BinderTypeView)]
 -> [(VarIdent, BinderTypeView)] -> [(VarIdent, BinderTypeView)])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(VarIdent, BinderTypeView)]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     ([(VarIdent, BinderTypeView)] -> [(VarIdent, BinderTypeView)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
binderTypesOfTerm (Decl n -> TermT n
forall (n :: S). Decl n -> TermT n
declType Decl n
decl)
       ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  ([(VarIdent, BinderTypeView)] -> [(VarIdent, BinderTypeView)])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(VarIdent, BinderTypeView)]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(VarIdent, BinderTypeView)]
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
<*> ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (State CheckLog))
  [(VarIdent, BinderTypeView)]
-> (TermT n
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         [(VarIdent, BinderTypeView)])
-> Maybe (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(VarIdent, BinderTypeView)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([(VarIdent, BinderTypeView)]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(VarIdent, BinderTypeView)]
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []) TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
binderTypesOfTerm (Decl n -> Maybe (TermT n)
forall (n :: S). Decl n -> Maybe (TermT n)
declValue Decl n
decl)

-- | The elaborated types of the local binders of one file's declarations, with the
-- rest of the run's declarations in scope so that 'whnfT' can unfold definitions
-- when splitting pair binders.
--
-- Pure at the interface: it runs the checker silently and returns no entries where
-- it fails.
binderTypesOfFile :: Checked -> FilePath -> [(VarIdent, BinderTypeView)]
binderTypesOfFile :: Checked -> String -> [(VarIdent, BinderTypeView)]
binderTypesOfFile (Checked Context n
ctx [(String, [Decl n])]
decls [TypeErrorInScopedContext]
_errs [CheckWarning]
_warnings) String
path =
  case Context n
-> TypeCheck n [(VarIdent, BinderTypeView)]
-> Either TypeErrorInScopedContext [(VarIdent, BinderTypeView)]
forall (n :: S) a.
Context n -> TypeCheck n a -> Either TypeErrorInScopedContext a
runTypeCheckIn Context n
ctx TypeCheck n [(VarIdent, BinderTypeView)]
action of
    Left TypeErrorInScopedContext
_        -> []
    Right [(VarIdent, BinderTypeView)]
entries -> [(VarIdent, BinderTypeView)]
entries
  where
    fileDecls :: [Decl n]
fileDecls = [[Decl n]] -> [Decl n]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Decl n]
ds | (String
p, [Decl n]
ds) <- [(String, [Decl n])]
decls, String
p String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
path ]
    action :: TypeCheck n [(VarIdent, BinderTypeView)]
action = Verbosity
-> TypeCheck n [(VarIdent, BinderTypeView)]
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall (n :: S) a. Verbosity -> TypeCheck n a -> TypeCheck n a
localVerbosity Verbosity
Silent (TypeCheck n [(VarIdent, BinderTypeView)]
 -> TypeCheck n [(VarIdent, BinderTypeView)])
-> TypeCheck n [(VarIdent, BinderTypeView)]
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall a b. (a -> b) -> a -> b
$
      [[(VarIdent, BinderTypeView)]] -> [(VarIdent, BinderTypeView)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(VarIdent, BinderTypeView)]] -> [(VarIdent, BinderTypeView)])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [[(VarIdent, BinderTypeView)]]
-> TypeCheck n [(VarIdent, BinderTypeView)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Decl n -> TypeCheck n [(VarIdent, BinderTypeView)])
-> [Decl n]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [[(VarIdent, BinderTypeView)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Decl n -> TypeCheck n [(VarIdent, BinderTypeView)]
forall (n :: S).
Distinct n =>
Decl n -> TypeCheck n [(VarIdent, BinderTypeView)]
declBinderTypes [Decl n]
fileDecls