{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Safe #-}
-- | Well-formedness checking for Eidos programs (doc/eidos.md §4): global
--   binder uniqueness, scoping, the spine discipline, bidirectional
--   (synthesis-plus-comparison) type checking, the join point discipline,
--   and the definition and program rules — all with located diagnostics.
--
--   The linter runs in one of three cumulative modes ('LintMode'),
--   corresponding to the pipeline's invariant stages (§4.1); the machine
--   level's rules are "ReWire.Synolon.Lint"'s, built on the expression
--   checker exported here:
--
--   * 'LintPoly' (post-bridge): the rules of §4.2–§4.4.
--   * 'LintMono' (post-specialization): additionally, every definition
--     signature is monomorphic and every type is nat-closed. Datatypes stay
--     parametric through specialization (§3.6), so constructor signatures
--     are exempt from the mono rules; 'Con' occurrences carry instantiated
--     types, which are not. Builtin-named definitions (rwPrim*) are the
--     builtins' type assumptions riding as polymorphic signature carriers
--     and check in poly mode. Value binders may still be higher-order here:
--     first-orderization is the partial evaluator's job, downstream of
--     specialization, so the first-order rule belongs to mono+ANF.
--   * 'LintMonoANF' (purify's input contract): additionally, value
--     binders are first-order and reactive definition bodies are in the
--     ANF shape of §6 (let chains over simple right-hand sides; the
--     reactive fragment — purify's input skeleton — is exempt from
--     naming, and pure definition bodies are exempt entirely — the fold
--     lowers them in any shape).
--
--   There is no inference and no unification anywhere: every binder carries
--   its type, so every expression synthesizes, and checking an expression
--   against a type is synthesis followed by structural comparison after
--   'natNorm'. This is the monadic, located-diagnostic twin of
--   'ReWire.Eidos.Types.typeOf', which is total on programs this module
--   accepts.
--
--   TODO(eidos): mono+ANF mode does not yet enforce the full
--   representable-closure type grammar of §4.1 (a permit-list of type
--   constructors — Vec, Finite, Bool, (), tuples, monomorphic ADTs,
--   Integer, Proxy, String in literal positions — plus
--   ReacT\/StateT\/Identity until purification); it checks the ANF shape,
--   first-order value binders, no-polymorphism, and nat-closure. The
--   Synolon lint enforces representability at a fixed bit width through
--   'envRepr'.
--   TODO(eidos): type arguments and constructor fields are not kind-checked
--   (there is no kind table for built-in type constructors); type-variable
--   occurrences are checked against their binders' kinds.
--   TODO(eidos): the builtin signature check ("ReWire.Eidos.BuiltinSigs")
--   is partial on type-level arithmetic: scheme subterms like
--   @Vec ((i + n) + m) a@ become deferred equations, checked only when
--   nat-closed on both sides after substitution. Shape and everything
--   matching binds directly are always checked.
module ReWire.Eidos.Lint
      ( LintMode (..), lint, lintDefn
        -- * The expression-level checker, for reuse by other checkers
      , Env (..), envFromDecls, bindVar, nonTail
      , checkExp, checkAgainst, checkTy, checkRepr, checkValueBinder, checkOccSig, checkDistinct
      , checkDataDefn, checkDefn, lookupCon, dconFieldTys
      , LitRep (..), litRep, fitsRep
      , declSites, expSites, idSite, tvSite
      ) where

import ReWire.Annotation (Annote, ann, noAnn)
import ReWire.Builtins (builtins)
import ReWire.Eidos.ANF (hasJump, isAtom, isPrimExp)
import ReWire.Eidos.BuiltinSigs (builtinSig, matchesSig)
import ReWire.Error (AstError, MonadError, failAt, failAtWith)
import ReWire.Eidos.Pretty ()
import ReWire.Eidos.Syntax
import ReWire.Eidos.Types (natNorm, tyEq, hasArrow, evalNat, instantiate, substTv, flattenApp, flattenArrow, flattenTyApp, reacOrStateT, typeOf)
import ReWire.Pretty (prettyPrint, showt)

import Control.Monad (foldM, foldM_, unless, when, zipWithM_)
import Data.Hashable (Hashable)
import Data.HashMap.Strict (HashMap)
import Data.HashSet (HashSet)
import Data.Text (Text)
import Numeric.Natural (Natural)

import qualified Data.HashMap.Strict as Map
import qualified Data.HashSet        as Set

-- | The linter's mode: which stage of the pipeline's cumulative static
--   discipline to enforce (doc/eidos.md §4.1). Modes are ordered by
--   strength.
data LintMode = LintPoly | LintMono | LintMonoANF
      deriving (LintMode -> LintMode -> Bool
(LintMode -> LintMode -> Bool)
-> (LintMode -> LintMode -> Bool) -> Eq LintMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LintMode -> LintMode -> Bool
== :: LintMode -> LintMode -> Bool
$c/= :: LintMode -> LintMode -> Bool
/= :: LintMode -> LintMode -> Bool
Eq, Eq LintMode
Eq LintMode =>
(LintMode -> LintMode -> Ordering)
-> (LintMode -> LintMode -> Bool)
-> (LintMode -> LintMode -> Bool)
-> (LintMode -> LintMode -> Bool)
-> (LintMode -> LintMode -> Bool)
-> (LintMode -> LintMode -> LintMode)
-> (LintMode -> LintMode -> LintMode)
-> Ord LintMode
LintMode -> LintMode -> Bool
LintMode -> LintMode -> Ordering
LintMode -> LintMode -> LintMode
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: LintMode -> LintMode -> Ordering
compare :: LintMode -> LintMode -> Ordering
$c< :: LintMode -> LintMode -> Bool
< :: LintMode -> LintMode -> Bool
$c<= :: LintMode -> LintMode -> Bool
<= :: LintMode -> LintMode -> Bool
$c> :: LintMode -> LintMode -> Bool
> :: LintMode -> LintMode -> Bool
$c>= :: LintMode -> LintMode -> Bool
>= :: LintMode -> LintMode -> Bool
$cmax :: LintMode -> LintMode -> LintMode
max :: LintMode -> LintMode -> LintMode
$cmin :: LintMode -> LintMode -> LintMode
min :: LintMode -> LintMode -> LintMode
Ord, Uniq -> LintMode -> ShowS
[LintMode] -> ShowS
LintMode -> String
(Uniq -> LintMode -> ShowS)
-> (LintMode -> String) -> ([LintMode] -> ShowS) -> Show LintMode
forall a.
(Uniq -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Uniq -> LintMode -> ShowS
showsPrec :: Uniq -> LintMode -> ShowS
$cshow :: LintMode -> String
show :: LintMode -> String
$cshowList :: [LintMode] -> ShowS
showList :: [LintMode] -> ShowS
Show)

-- | Check a whole program in the given mode; succeeds exactly when every
--   rule of the mode holds.
lint :: MonadError AstError m => LintMode -> Program -> m ()
lint :: forall (m :: * -> *).
MonadError AstError m =>
LintMode -> Program -> m ()
lint LintMode
mode Program
p = Env -> Program -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Program -> m ()
checkProgram (LintMode -> Program -> Env
mkEnv LintMode
mode Program
p) Program
p

-- | Check a single definition against a program's global context: every
--   rule except the whole-program ones (global binder uniqueness, global
--   name distinctness, datatype well-formedness, and the @top@ rule).
lintDefn :: MonadError AstError m => LintMode -> Program -> Defn -> m ()
lintDefn :: forall (m :: * -> *).
MonadError AstError m =>
LintMode -> Program -> Defn -> m ()
lintDefn LintMode
mode Program
p Defn
d = Env -> Defn -> m ()
forall (m :: * -> *). MonadError AstError m => Env -> Defn -> m ()
checkDefn (LintMode -> Program -> Env
mkEnv LintMode
mode Program
p) Defn
d

---
--- Environments.
---

-- | A join point visible in the current scope: its declared 'JoinId', its
--   parameter types, and its result type (the type of its scope).
data JoinDef = JoinDef !JoinId ![Ty] !Ty

data Env = Env
      { Env -> LintMode
envMode        :: LintMode
      , Env -> Bool
envBanReactive :: Bool                       -- ^ the reactive types are out of the type grammar (the machine level)
      , Env -> Maybe (Ty -> Either TyConId Natural)
envRepr        :: Maybe (Ty -> Either Text Natural) -- ^ the representable closure: the width of a type, or why it has none (the machine level)
      , Env -> HashMap TyConId (TyConId, Sig)
envCons  :: HashMap DataConId (TyConId, Sig) -- ^ data constructors, by name
      , Env -> HashMap Uniq Id
envScope :: HashMap Uniq Id                  -- ^ term binders in scope
      , Env -> HashMap Uniq TyVar
envTVs   :: HashMap Uniq TyVar               -- ^ signature type variables in scope
      , Env -> HashMap Uniq JoinDef
envJoins :: HashMap Uniq JoinDef             -- ^ join points lexically visible
      , Env -> HashSet Uniq
envTail  :: HashSet Uniq                     -- ^ joins jumpable from here (tail position of their scopes)
      }

mkEnv :: LintMode -> Program -> Env
mkEnv :: LintMode -> Program -> Env
mkEnv LintMode
mode (Program [DataDefn]
datas [Defn]
defns Id
_) = LintMode -> [DataDefn] -> [Defn] -> Env
envFromDecls LintMode
mode [DataDefn]
datas [Defn]
defns

-- | The checking environment over a datatype and definition table: the
--   whole-program scope every rule starts from.
envFromDecls :: LintMode -> [DataDefn] -> [Defn] -> Env
envFromDecls :: LintMode -> [DataDefn] -> [Defn] -> Env
envFromDecls LintMode
mode [DataDefn]
datas [Defn]
defns = Env
      { envMode :: LintMode
envMode  = LintMode
mode
      , envBanReactive :: Bool
envBanReactive = Bool
False
      , envRepr :: Maybe (Ty -> Either TyConId Natural)
envRepr  = Maybe (Ty -> Either TyConId Natural)
forall a. Maybe a
Nothing
      , envCons :: HashMap TyConId (TyConId, Sig)
envCons  = [(TyConId, (TyConId, Sig))] -> HashMap TyConId (TyConId, Sig)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList [ (TyConId
c, (DataDefn -> TyConId
dataName DataDefn
d, Sig
sig)) | DataDefn
d <- [DataDefn]
datas, DataCon Annote
_ TyConId
c Sig
sig <- DataDefn -> [DataCon]
dataCons DataDefn
d ]
      , envScope :: HashMap Uniq Id
envScope = [(Uniq, Id)] -> HashMap Uniq Id
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList [ (Id -> Uniq
idUniq (Id -> Uniq) -> Id -> Uniq
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d, Defn -> Id
defnId Defn
d) | Defn
d <- [Defn]
defns ]
      , envTVs :: HashMap Uniq TyVar
envTVs   = HashMap Uniq TyVar
forall a. Monoid a => a
mempty
      , envJoins :: HashMap Uniq JoinDef
envJoins = HashMap Uniq JoinDef
forall a. Monoid a => a
mempty
      , envTail :: HashSet Uniq
envTail  = HashSet Uniq
forall a. Monoid a => a
mempty
      }

bindVar :: Id -> Env -> Env
bindVar :: Id -> Env -> Env
bindVar Id
x Env
env = Env
env { envScope = Map.insert (idUniq x) x $ envScope env }

-- | Make a join point lexically visible without making it jumpable (used
--   for its own body: join points are not recursive).
scopeJoin :: Id -> JoinDef -> Env -> Env
scopeJoin :: Id -> JoinDef -> Env -> Env
scopeJoin Id
x JoinDef
jd Env
env = Env
env { envJoins = Map.insert (idUniq x) jd $ envJoins env }

-- | Make a join point visible and jumpable (used for its scope: the let
--   body, whose tail is the join's tail).
bindJoin :: Id -> JoinDef -> Env -> Env
bindJoin :: Id -> JoinDef -> Env -> Env
bindJoin Id
x JoinDef
jd Env
env = (Id -> JoinDef -> Env -> Env
scopeJoin Id
x JoinDef
jd Env
env) { envTail = Set.insert (idUniq x) $ envTail env }

-- | Entering a non-tail position: no join is jumpable from here (they stay
--   visible, for diagnostics), though joins bound inside are jumpable
--   within their own scopes.
nonTail :: Env -> Env
nonTail :: Env -> Env
nonTail Env
env = Env
env { envTail = mempty }

---
--- Programs.
---

checkProgram :: MonadError AstError m => Env -> Program -> m ()
checkProgram :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Program -> m ()
checkProgram Env
env p :: Program
p@(Program [DataDefn]
datas [Defn]
defns Id
top) = do
      [(Uniq, Annote, TyConId)] -> m ()
forall k (m :: * -> *).
(MonadError AstError m, Eq k, Hashable k) =>
[(k, Annote, TyConId)] -> m ()
checkDistinct ([(Uniq, Annote, TyConId)] -> m ())
-> [(Uniq, Annote, TyConId)] -> m ()
forall a b. (a -> b) -> a -> b
$ Program -> [(Uniq, Annote, TyConId)]
uniqSites Program
p
      [(TyConId, Annote, TyConId)] -> m ()
forall k (m :: * -> *).
(MonadError AstError m, Eq k, Hashable k) =>
[(k, Annote, TyConId)] -> m ()
checkDistinct [ (DataDefn -> TyConId
dataName DataDefn
d, DataDefn -> Annote
dataAnnote DataDefn
d, TyConId
"datatype name " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> DataDefn -> TyConId
dataName DataDefn
d) | DataDefn
d <- [DataDefn]
datas ]
      [(TyConId, Annote, TyConId)] -> m ()
forall k (m :: * -> *).
(MonadError AstError m, Eq k, Hashable k) =>
[(k, Annote, TyConId)] -> m ()
checkDistinct [ (TyConId
c, Annote
an, TyConId
"data constructor name " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
c) | DataDefn
d <- [DataDefn]
datas, DataCon Annote
an TyConId
c Sig
_ <- DataDefn -> [DataCon]
dataCons DataDefn
d ]
      (DataDefn -> m ()) -> [DataDefn] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Env -> DataDefn -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> DataDefn -> m ()
checkDataDefn Env
env) [DataDefn]
datas
      (Defn -> m ()) -> [Defn] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Env -> Defn -> m ()
forall (m :: * -> *). MonadError AstError m => Env -> Defn -> m ()
checkDefn Env
env) [Defn]
defns
      Env -> [Defn] -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> [Defn] -> Id -> m ()
checkTop Env
env [Defn]
defns Id
top

-- | @top@ resolves to a definition, its occurrence signature matches the
--   binder's, and (in mono mode) the definition has the device type
--   @ReacT i o Identity a@ (doc/eidos.md §4.3; the result type is
--   unconstrained — a non-halting device never produces it).
checkTop :: MonadError AstError m => Env -> [Defn] -> Id -> m ()
checkTop :: forall (m :: * -> *).
MonadError AstError m =>
Env -> [Defn] -> Id -> m ()
checkTop Env
env [Defn]
defns Id
top = case [ Defn
d | Defn
d <- [Defn]
defns, Id -> Uniq
idUniq (Defn -> Id
defnId Defn
d) Uniq -> Uniq -> Bool
forall a. Eq a => a -> a -> Bool
== Id -> Uniq
idUniq Id
top ] of
      []    -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
noAnn (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"top: designated device root " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
top TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" does not name a definition"
      Defn
d : [Defn]
_ -> do
            Annote -> Id -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Annote -> Id -> Id -> m ()
checkOccSig (Defn -> Annote
defnAnnote Defn
d) Id
top (Id -> m ()) -> Id -> m ()
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d
            Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Env -> LintMode
envMode Env
env LintMode -> LintMode -> Bool
forall a. Ord a => a -> a -> Bool
>= LintMode
LintMono) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> Ty -> m ()
forall (m :: * -> *). MonadError AstError m => Annote -> Ty -> m ()
checkDeviceTy (Defn -> Annote
defnAnnote Defn
d) (Ty -> m ()) -> Ty -> m ()
forall a b. (a -> b) -> a -> b
$ Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig (Id -> Sig) -> Id -> Sig
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d
      where checkDeviceTy :: MonadError AstError m => Annote -> Ty -> m ()
            checkDeviceTy :: forall (m :: * -> *). MonadError AstError m => Annote -> Ty -> m ()
checkDeviceTy Annote
an Ty
t = case Ty -> (Ty, [Ty])
flattenTyApp (Ty -> (Ty, [Ty])) -> Ty -> (Ty, [Ty])
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
natNorm Ty
t of
                  (TyCon Annote
_ TyConId
"ReacT", [Ty
_, Ty
_, TyCon Annote
_ TyConId
"Identity", Ty
_]) -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                  (Ty, [Ty])
_ -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"the top definition must have type ReacT i o Identity a, not " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
t

---
--- Global binder uniqueness (doc/eidos.md §2, §4.4).
---

-- | Fold a list of keyed sites, reporting the first duplicate with both
--   locations.
checkDistinct :: forall k m. (MonadError AstError m, Eq k, Hashable k) => [(k, Annote, Text)] -> m ()
checkDistinct :: forall k (m :: * -> *).
(MonadError AstError m, Eq k, Hashable k) =>
[(k, Annote, TyConId)] -> m ()
checkDistinct = (HashMap k (Annote, TyConId)
 -> (k, Annote, TyConId) -> m (HashMap k (Annote, TyConId)))
-> HashMap k (Annote, TyConId) -> [(k, Annote, TyConId)] -> m ()
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ HashMap k (Annote, TyConId)
-> (k, Annote, TyConId) -> m (HashMap k (Annote, TyConId))
ins HashMap k (Annote, TyConId)
forall a. Monoid a => a
mempty
      where ins :: HashMap k (Annote, Text) -> (k, Annote, Text) -> m (HashMap k (Annote, Text))
            ins :: HashMap k (Annote, TyConId)
-> (k, Annote, TyConId) -> m (HashMap k (Annote, TyConId))
ins HashMap k (Annote, TyConId)
seen (k
k, Annote
an, TyConId
what) = case k -> HashMap k (Annote, TyConId) -> Maybe (Annote, TyConId)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup k
k HashMap k (Annote, TyConId)
seen of
                  Just (Annote
an', TyConId
what') -> Annote
-> TyConId
-> [(Annote, TyConId)]
-> [TyConId]
-> m (HashMap k (Annote, TyConId))
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> [(Annote, TyConId)] -> [TyConId] -> m a
failAtWith Annote
an (TyConId
"duplicate " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
what)
                        [(Annote
an', TyConId
"first introduced here: " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
what')] []
                  Maybe (Annote, TyConId)
Nothing           -> HashMap k (Annote, TyConId) -> m (HashMap k (Annote, TyConId))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HashMap k (Annote, TyConId) -> m (HashMap k (Annote, TyConId)))
-> HashMap k (Annote, TyConId) -> m (HashMap k (Annote, TyConId))
forall a b. (a -> b) -> a -> b
$ k
-> (Annote, TyConId)
-> HashMap k (Annote, TyConId)
-> HashMap k (Annote, TyConId)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert k
k (Annote
an, TyConId
what) HashMap k (Annote, TyConId)
seen

-- | Every binding site in the program, in deterministic order: definition
--   names, signature type variables, parameters, all local binders, and
--   datatype parameters. Occurrences (which share their binder's unique)
--   contribute nothing.
uniqSites :: Program -> [(Uniq, Annote, Text)]
uniqSites :: Program -> [(Uniq, Annote, TyConId)]
uniqSites (Program [DataDefn]
datas [Defn]
defns Id
_) = [DataDefn] -> [Defn] -> [(Uniq, Annote, TyConId)]
declSites [DataDefn]
datas [Defn]
defns

-- | Every binding site of the datatype-and-definition fragment, in
--   deterministic order.
declSites :: [DataDefn] -> [Defn] -> [(Uniq, Annote, Text)]
declSites :: [DataDefn] -> [Defn] -> [(Uniq, Annote, TyConId)]
declSites [DataDefn]
datas [Defn]
defns = (DataDefn -> [(Uniq, Annote, TyConId)])
-> [DataDefn] -> [(Uniq, Annote, TyConId)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataDefn -> [(Uniq, Annote, TyConId)]
dataSites [DataDefn]
datas [(Uniq, Annote, TyConId)]
-> [(Uniq, Annote, TyConId)] -> [(Uniq, Annote, TyConId)]
forall a. Semigroup a => a -> a -> a
<> (Defn -> [(Uniq, Annote, TyConId)])
-> [Defn] -> [(Uniq, Annote, TyConId)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Defn -> [(Uniq, Annote, TyConId)]
defnSites [Defn]
defns
      where -- Constructors of one datatype share the datatype's parameter
            -- uniques ('checkDataDefn' enforces that their quantifier lists
            -- coincide), so only the first constructor's list contributes
            -- binding sites.
            dataSites :: DataDefn -> [(Uniq, Annote, Text)]
            dataSites :: DataDefn -> [(Uniq, Annote, TyConId)]
dataSites DataDefn
d = case DataDefn -> [DataCon]
dataCons DataDefn
d of
                  DataCon Annote
an TyConId
_ (Sig [TyVar]
tvs Ty
_) : [DataCon]
_ -> (TyVar -> (Uniq, Annote, TyConId))
-> [TyVar] -> [(Uniq, Annote, TyConId)]
forall a b. (a -> b) -> [a] -> [b]
map (Annote -> TyConId -> TyVar -> (Uniq, Annote, TyConId)
tvSite Annote
an TyConId
"datatype parameter") [TyVar]
tvs
                  []                           -> []

            defnSites :: Defn -> [(Uniq, Annote, Text)]
            defnSites :: Defn -> [(Uniq, Annote, TyConId)]
defnSites (Defn Annote
an Id
x [Id]
ps Exp
body Maybe DefnAttr
_ Maybe SpecOrigin
_) =
                  Annote -> TyConId -> Id -> (Uniq, Annote, TyConId)
idSite Annote
an TyConId
"definition name" Id
x
                        (Uniq, Annote, TyConId)
-> [(Uniq, Annote, TyConId)] -> [(Uniq, Annote, TyConId)]
forall a. a -> [a] -> [a]
: (TyVar -> (Uniq, Annote, TyConId))
-> [TyVar] -> [(Uniq, Annote, TyConId)]
forall a b. (a -> b) -> [a] -> [b]
map (Annote -> TyConId -> TyVar -> (Uniq, Annote, TyConId)
tvSite Annote
an TyConId
"signature type variable") (Sig -> [TyVar]
sigTVs (Sig -> [TyVar]) -> Sig -> [TyVar]
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
x)
                        [(Uniq, Annote, TyConId)]
-> [(Uniq, Annote, TyConId)] -> [(Uniq, Annote, TyConId)]
forall a. Semigroup a => a -> a -> a
<> (Id -> (Uniq, Annote, TyConId))
-> [Id] -> [(Uniq, Annote, TyConId)]
forall a b. (a -> b) -> [a] -> [b]
map (Annote -> TyConId -> Id -> (Uniq, Annote, TyConId)
idSite Annote
an TyConId
"parameter") [Id]
ps
                        [(Uniq, Annote, TyConId)]
-> [(Uniq, Annote, TyConId)] -> [(Uniq, Annote, TyConId)]
forall a. Semigroup a => a -> a -> a
<> Exp -> [(Uniq, Annote, TyConId)]
expSites Exp
body

-- | Every binding site inside an expression.
expSites :: Exp -> [(Uniq, Annote, Text)]
expSites :: Exp -> [(Uniq, Annote, TyConId)]
expSites = \ case
      Var {}             -> []
      Con {}             -> []
      Prim {}            -> []
      LitInt {}          -> []
      LitStr {}          -> []
      LitList Annote
_ Ty
_ [Exp]
es     -> (Exp -> [(Uniq, Annote, TyConId)])
-> [Exp] -> [(Uniq, Annote, TyConId)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Exp -> [(Uniq, Annote, TyConId)]
expSites [Exp]
es
      LitVec Annote
_ Ty
_ [Exp]
es      -> (Exp -> [(Uniq, Annote, TyConId)])
-> [Exp] -> [(Uniq, Annote, TyConId)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Exp -> [(Uniq, Annote, TyConId)]
expSites [Exp]
es
      App Annote
_ Exp
e Arg
a          -> Exp -> [(Uniq, Annote, TyConId)]
expSites Exp
e [(Uniq, Annote, TyConId)]
-> [(Uniq, Annote, TyConId)] -> [(Uniq, Annote, TyConId)]
forall a. Semigroup a => a -> a -> a
<> Arg -> [(Uniq, Annote, TyConId)]
argSites Arg
a
      Lam Annote
an Id
x Exp
e         -> Annote -> TyConId -> Id -> (Uniq, Annote, TyConId)
idSite Annote
an TyConId
"lambda parameter" Id
x (Uniq, Annote, TyConId)
-> [(Uniq, Annote, TyConId)] -> [(Uniq, Annote, TyConId)]
forall a. a -> [a] -> [a]
: Exp -> [(Uniq, Annote, TyConId)]
expSites Exp
e
      Let Annote
an Bind
b Exp
e         -> Annote -> Bind -> [(Uniq, Annote, TyConId)]
bindSites Annote
an Bind
b [(Uniq, Annote, TyConId)]
-> [(Uniq, Annote, TyConId)] -> [(Uniq, Annote, TyConId)]
forall a. Semigroup a => a -> a -> a
<> Exp -> [(Uniq, Annote, TyConId)]
expSites Exp
e
      Jump Annote
_ JoinId
_ [Exp]
es        -> (Exp -> [(Uniq, Annote, TyConId)])
-> [Exp] -> [(Uniq, Annote, TyConId)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Exp -> [(Uniq, Annote, TyConId)]
expSites [Exp]
es
      Case Annote
an Ty
_ Exp
e Id
x [Alt]
alts -> Exp -> [(Uniq, Annote, TyConId)]
expSites Exp
e [(Uniq, Annote, TyConId)]
-> [(Uniq, Annote, TyConId)] -> [(Uniq, Annote, TyConId)]
forall a. Semigroup a => a -> a -> a
<> (Annote -> TyConId -> Id -> (Uniq, Annote, TyConId)
idSite Annote
an TyConId
"case binder" Id
x (Uniq, Annote, TyConId)
-> [(Uniq, Annote, TyConId)] -> [(Uniq, Annote, TyConId)]
forall a. a -> [a] -> [a]
: (Alt -> [(Uniq, Annote, TyConId)])
-> [Alt] -> [(Uniq, Annote, TyConId)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Alt -> [(Uniq, Annote, TyConId)]
altSites [Alt]
alts)
      where argSites :: Arg -> [(Uniq, Annote, Text)]
            argSites :: Arg -> [(Uniq, Annote, TyConId)]
argSites = \ case
                  EArg Exp
e -> Exp -> [(Uniq, Annote, TyConId)]
expSites Exp
e
                  TArg Ty
_ -> []

            bindSites :: Annote -> Bind -> [(Uniq, Annote, Text)]
            bindSites :: Annote -> Bind -> [(Uniq, Annote, TyConId)]
bindSites Annote
an = \ case
                  NonRec Id
x Exp
e  -> Annote -> TyConId -> Id -> (Uniq, Annote, TyConId)
idSite Annote
an TyConId
"let binder" Id
x (Uniq, Annote, TyConId)
-> [(Uniq, Annote, TyConId)] -> [(Uniq, Annote, TyConId)]
forall a. a -> [a] -> [a]
: Exp -> [(Uniq, Annote, TyConId)]
expSites Exp
e
                  Rec [(Id, Exp)]
bs      -> ((Id, Exp) -> [(Uniq, Annote, TyConId)])
-> [(Id, Exp)] -> [(Uniq, Annote, TyConId)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Id
x, Exp
e) -> Annote -> TyConId -> Id -> (Uniq, Annote, TyConId)
idSite Annote
an TyConId
"recursive let binder" Id
x (Uniq, Annote, TyConId)
-> [(Uniq, Annote, TyConId)] -> [(Uniq, Annote, TyConId)]
forall a. a -> [a] -> [a]
: Exp -> [(Uniq, Annote, TyConId)]
expSites Exp
e) [(Id, Exp)]
bs
                  Join JoinId
j [Id]
xs Exp
e -> Annote -> TyConId -> Id -> (Uniq, Annote, TyConId)
idSite Annote
an TyConId
"join point" (JoinId -> Id
jpId JoinId
j)
                        (Uniq, Annote, TyConId)
-> [(Uniq, Annote, TyConId)] -> [(Uniq, Annote, TyConId)]
forall a. a -> [a] -> [a]
: (Id -> (Uniq, Annote, TyConId))
-> [Id] -> [(Uniq, Annote, TyConId)]
forall a b. (a -> b) -> [a] -> [b]
map (Annote -> TyConId -> Id -> (Uniq, Annote, TyConId)
idSite Annote
an TyConId
"join point parameter") [Id]
xs
                        [(Uniq, Annote, TyConId)]
-> [(Uniq, Annote, TyConId)] -> [(Uniq, Annote, TyConId)]
forall a. Semigroup a => a -> a -> a
<> Exp -> [(Uniq, Annote, TyConId)]
expSites Exp
e

            altSites :: Alt -> [(Uniq, Annote, Text)]
            altSites :: Alt -> [(Uniq, Annote, TyConId)]
altSites (Alt Annote
an AltCon
_ [Id]
xs Exp
e) = (Id -> (Uniq, Annote, TyConId))
-> [Id] -> [(Uniq, Annote, TyConId)]
forall a b. (a -> b) -> [a] -> [b]
map (Annote -> TyConId -> Id -> (Uniq, Annote, TyConId)
idSite Annote
an TyConId
"pattern binder") [Id]
xs [(Uniq, Annote, TyConId)]
-> [(Uniq, Annote, TyConId)] -> [(Uniq, Annote, TyConId)]
forall a. Semigroup a => a -> a -> a
<> Exp -> [(Uniq, Annote, TyConId)]
expSites Exp
e

-- | A term binding site, keyed by unique, with its diagnostic text.
idSite :: Annote -> Text -> Id -> (Uniq, Annote, Text)
idSite :: Annote -> TyConId -> Id -> (Uniq, Annote, TyConId)
idSite Annote
an TyConId
what Id
x = (Id -> Uniq
idUniq Id
x, Annote
an, TyConId
"binding unique #" TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Uniq -> TyConId
forall a. TextShow a => a -> TyConId
showt (Id -> Uniq
idUniq Id
x) TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" (" TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
what TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
x TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
")")

-- | A type-variable binding site, keyed by unique, with its diagnostic text.
tvSite :: Annote -> Text -> TyVar -> (Uniq, Annote, Text)
tvSite :: Annote -> TyConId -> TyVar -> (Uniq, Annote, TyConId)
tvSite Annote
an TyConId
what TyVar
v = (TyVar -> Uniq
tvUniq TyVar
v, Annote
an, TyConId
"binding unique #" TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Uniq -> TyConId
forall a. TextShow a => a -> TyConId
showt (TyVar -> Uniq
tvUniq TyVar
v) TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" (" TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
what TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyVar -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint TyVar
v TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
")")

---
--- Datatypes (doc/eidos.md §3.6, §4.3).
---

-- | The datatype's kind constructs @*@ from its parameter kinds; every
--   constructor quantifies exactly the datatype's parameters (the same
--   type variables, in the same order, across all constructors) and
--   constructs exactly the datatype applied to them.
checkDataDefn :: forall m. MonadError AstError m => Env -> DataDefn -> m ()
checkDataDefn :: forall (m :: * -> *).
MonadError AstError m =>
Env -> DataDefn -> m ()
checkDataDefn Env
env (DataDefn Annote
an TyConId
t Kind
k [DataCon]
cs) = do
      let ([Kind]
doms, Kind
kres) = Kind -> ([Kind], Kind)
kindSpine Kind
k
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
kres Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KStar) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"datatype " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
t TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
": kind must construct *"
      case [DataCon]
cs of
            []                              -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            DataCon Annote
_ TyConId
_ (Sig [TyVar]
tvs0 Ty
_) : [DataCon]
_    -> (DataCon -> m ()) -> [DataCon] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Kind] -> [TyVar] -> DataCon -> m ()
checkCtor [Kind]
doms [TyVar]
tvs0) [DataCon]
cs
      where checkCtor :: [Kind] -> [TyVar] -> DataCon -> m ()
            checkCtor :: [Kind] -> [TyVar] -> DataCon -> m ()
checkCtor [Kind]
doms [TyVar]
tvs0 (DataCon Annote
an' TyConId
c (Sig [TyVar]
tvs Ty
ty)) = do
                  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TyVar]
tvs [TyVar] -> [TyVar] -> Bool
forall a. Eq a => a -> a -> Bool
== [TyVar]
tvs0) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an'
                        (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"constructor " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
c TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
": quantified type variables differ across constructors of " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
t
                  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TyVar] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [TyVar]
tvs Uniq -> Uniq -> Bool
forall a. Eq a => a -> a -> Bool
== [Kind] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Kind]
doms) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an'
                        (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"constructor " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
c TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
": quantifies " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Uniq -> TyConId
forall a. TextShow a => a -> TyConId
showt ([TyVar] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [TyVar]
tvs)
                        TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" type variables but the kind of " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
t TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" has " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Uniq -> TyConId
forall a. TextShow a => a -> TyConId
showt ([Kind] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Kind]
doms) TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" parameters"
                  (TyVar -> Kind -> m ()) -> [TyVar] -> [Kind] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (\ TyVar
v Kind
kd -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TyVar -> Kind
tvKind TyVar
v Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
kd) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an'
                              (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"constructor " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
c TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
": the kind of type variable " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyVar -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint TyVar
v
                              TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" does not match the corresponding parameter of the kind of " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
t)
                        [TyVar]
tvs [Kind]
doms
                  -- Datatypes stay parametric through specialization, so
                  -- constructor signatures see only the scoping rules (no
                  -- mono-mode closedness).
                  Env -> Annote -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTyScope (Env
env { envTVs = Map.fromList [ (tvUniq v, v) | v <- tvs ] }) Annote
an' Ty
ty
                  case Ty -> (Ty, [Ty])
flattenTyApp (Ty -> (Ty, [Ty])) -> Ty -> (Ty, [Ty])
forall a b. (a -> b) -> a -> b
$ ([Ty], Ty) -> Ty
forall a b. (a, b) -> b
snd (([Ty], Ty) -> Ty) -> ([Ty], Ty) -> Ty
forall a b. (a -> b) -> a -> b
$ Ty -> ([Ty], Ty)
flattenArrow Ty
ty of
                        (TyCon Annote
_ TyConId
t', [Ty]
args) | TyConId
t' TyConId -> TyConId -> Bool
forall a. Eq a => a -> a -> Bool
== TyConId
t, [Ty]
args [Ty] -> [Ty] -> Bool
forall a. Eq a => a -> a -> Bool
== (TyVar -> Ty) -> [TyVar] -> [Ty]
forall a b. (a -> b) -> [a] -> [b]
map (Annote -> TyVar -> Ty
TyVarT Annote
an') [TyVar]
tvs -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                        (Ty, [Ty])
_ -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an' (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"constructor " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
c TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" must construct " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
t
                              TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" applied to exactly its quantified type variables"

            kindSpine :: Kind -> ([Kind], Kind)
            kindSpine :: Kind -> ([Kind], Kind)
kindSpine = \ case
                  KFun Kind
k1 Kind
k2 -> let ([Kind]
ks, Kind
r) = Kind -> ([Kind], Kind)
kindSpine Kind
k2 in (Kind
k1 Kind -> [Kind] -> [Kind]
forall a. a -> [a] -> [a]
: [Kind]
ks, Kind
r)
                  Kind
k'         -> ([], Kind
k')

---
--- Definitions (doc/eidos.md §3.5, §4.3).
---

-- | Parameters match a prefix of the signature's arrow spine; the body
--   checks against the remainder. In mono mode the signature quantifies
--   nothing — except the builtin-named definitions (rwPrim*), which are
--   the builtins' type assumptions riding to the Eidos-to-Hyle fold as
--   polymorphic signature carriers (error-stub bodies, never referenced
--   as variables); they check in poly mode. In mono+ANF mode the body
--   must additionally be in the ANF shape of doc/eidos.md §6
--   ('checkANF').
checkDefn :: MonadError AstError m => Env -> Defn -> m ()
checkDefn :: forall (m :: * -> *). MonadError AstError m => Env -> Defn -> m ()
checkDefn Env
env0 d :: Defn
d@(Defn Annote
_ Id
x0 [Id]
_ Exp
_ Maybe DefnAttr
_ Maybe SpecOrigin
_)
      | Env -> LintMode
envMode Env
env0 LintMode -> LintMode -> Bool
forall a. Ord a => a -> a -> Bool
>= LintMode
LintMono, TyConId -> HashSet TyConId -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
Set.member (Id -> TyConId
idOcc Id
x0) HashSet TyConId
primNames = Env -> Defn -> m ()
forall (m :: * -> *). MonadError AstError m => Env -> Defn -> m ()
checkDefn' (Env
env0 { envMode = LintPoly, envRepr = Nothing }) Defn
d
      | Bool
otherwise = do
            Env -> Defn -> m ()
forall (m :: * -> *). MonadError AstError m => Env -> Defn -> m ()
checkDefn' Env
env0 Defn
d
            -- Only the reactive fragment is A-normalized (the fold
            -- lowers pure expressions in any shape).
            Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Env -> LintMode
envMode Env
env0 LintMode -> LintMode -> Bool
forall a. Eq a => a -> a -> Bool
== LintMode
LintMonoANF Bool -> Bool -> Bool
&& Ty -> Bool
reacOrStateT (Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
x0)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Defn -> m ()
forall (m :: * -> *). MonadError AstError m => Defn -> m ()
checkANF Defn
d
      where primNames :: HashSet Text
            primNames :: HashSet TyConId
primNames = [TyConId] -> HashSet TyConId
forall a. (Eq a, Hashable a) => [a] -> HashSet a
Set.fromList ([TyConId] -> HashSet TyConId) -> [TyConId] -> HashSet TyConId
forall a b. (a -> b) -> a -> b
$ ((TyConId, Builtin) -> TyConId)
-> [(TyConId, Builtin)] -> [TyConId]
forall a b. (a -> b) -> [a] -> [b]
map (TyConId, Builtin) -> TyConId
forall a b. (a, b) -> a
fst [(TyConId, Builtin)]
builtins

-- | The ANF shape (doc/eidos.md §6): a definition body is a let chain
--   over simple right-hand sides ending in an atom, a jump, a reactive
--   spine, or a reactive case — the reactive fragment is exempt from
--   naming (it is purify's input skeleton): reactive spines keep lambda
--   (continuation) arguments and in-place reactive arguments; a reactive
--   case stays in tail position. Types were already checked; this is
--   purely structural.
checkANF :: forall m. MonadError AstError m => Defn -> m ()
checkANF :: forall (m :: * -> *). MonadError AstError m => Defn -> m ()
checkANF Defn
d = Exp -> m ()
tailOk (Exp -> m ()) -> Exp -> m ()
forall a b. (a -> b) -> a -> b
$ Defn -> Exp
defnBody Defn
d
      where tailOk :: Exp -> m ()
            tailOk :: Exp -> m ()
tailOk Exp
e = case Exp
e of
                  Exp
_ | Exp -> Bool
atomOk Exp
e -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                  Jump Annote
an JoinId
_ [Exp]
es -> (Exp -> m ()) -> [Exp] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Annote -> TyConId -> Exp -> m ()
atom Annote
an TyConId
"jump argument") [Exp]
es
                  Let Annote
_ (NonRec Id
_ Exp
r) Exp
body -> Exp -> m ()
rOk Exp
r m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Exp -> m ()
tailOk Exp
body
                  Let Annote
_ (Join JoinId
_ [Id]
_ Exp
b) Exp
body -> Exp -> m ()
tailOk Exp
b m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Exp -> m ()
tailOk Exp
body
                  Case Annote
an Ty
t Exp
_ Id
_ [Alt]
_
                        | Ty -> Bool
reacOrStateT Ty
t Bool -> Bool -> Bool
|| Exp -> Bool
hasJump Exp
e -> Exp -> m ()
caseOk Exp
e
                        | Bool
otherwise -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an TyConId
"ANF: a pure case in tail position (must be let-bound)"
                  App {}
                        | Ty -> Bool
reacOrStateT (Exp -> Ty
typeOf Exp
e) Bool -> Bool -> Bool
|| Ty -> Bool
hasArrow (Exp -> Ty
typeOf Exp
e) -> Exp -> m ()
spineOk Exp
e
                        | Bool
otherwise -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
e) TyConId
"ANF: a pure application in tail position (must be let-bound)"
                  Lam Annote
_ Id
_ Exp
b -> Exp -> m ()
tailOk Exp
b -- residual reactive-continuation lambda
                  Exp
_ -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
e) TyConId
"ANF: not a let chain ending in an atom, jump, or reactive tail"

            rOk :: Exp -> m ()
            rOk :: Exp -> m ()
rOk Exp
r = case Exp
r of
                  Exp
_ | Exp -> Bool
atomOk Exp
r -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                  Case {}      -> Exp -> m ()
caseOk Exp
r
                  App {}       -> Exp -> m ()
spineOk Exp
r
                  Lam {}       -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- never minted on the pipeline; tolerated in fixtures
                  Exp
_            -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
r) TyConId
"ANF: right-hand side is not a simple computation"

            caseOk :: Exp -> m ()
            caseOk :: Exp -> m ()
caseOk (Case Annote
an Ty
_ Exp
s Id
_ [Alt]
alts) = do
                  Annote -> TyConId -> Exp -> m ()
atom Annote
an TyConId
"case scrutinee" Exp
s
                  (Alt -> m ()) -> [Alt] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Alt Annote
_ AltCon
_ [Id]
_ Exp
b) -> Exp -> m ()
tailOk Exp
b) [Alt]
alts
            caseOk Exp
e = Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
e) TyConId
"ANF: expected a case (rwc bug)"

            -- The head is a variable, constructor, or primitive (a
            -- lambda head is a residual beta-redex, which normalization
            -- turns into a let); arguments are atoms, except the
            -- naming-exempt forms, all normalized in place: primitive
            -- expressions (transparent, nesting freely), lambda and
            -- function-typed arguments (continuations, higher-order
            -- primitive arguments, partial applications), and reactive
            -- arguments.
            spineOk :: Exp -> m ()
            spineOk :: Exp -> m ()
spineOk Exp
e = do
                  let (Exp
h, [Arg]
args) = Exp -> (Exp, [Arg])
flattenApp Exp
e
                  case Exp
h of
                        Var {}  -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                        Con {}  -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                        Prim {} -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                        Lam {}  -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
e) TyConId
"ANF: a residual beta-redex (the application's lambda head must be let-bound)"
                        Exp
_       -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
e) TyConId
"ANF: the application's head is not a variable, constructor, or primitive"
                  (Exp -> m ()) -> [Exp] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Exp -> m ()
argOk [ Exp
a | EArg Exp
a <- [Arg]
args ]
                  where argOk :: Exp -> m ()
                        argOk :: Exp -> m ()
argOk Exp
a
                              | Exp -> Bool
atomOk Exp
a                = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                              | Lam {} <- Exp
a             = Exp -> m ()
tailOk Exp
a
                              | Exp -> Bool
isPrimExp Exp
a             = Exp -> m ()
spineOk Exp
a
                              | Ty -> Bool
hasArrow (Ty -> Bool) -> Ty -> Bool
forall a b. (a -> b) -> a -> b
$ Exp -> Ty
typeOf Exp
a     = case Exp
a of
                                    App {}  -> Exp -> m ()
spineOk Exp
a
                                    Con {}  -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- a bare constructor reference
                                    Prim {} -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- a bare operator primitive
                                    Exp
_       -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
a) TyConId
"ANF: a function-typed argument must be a lambda, a partial application, or a definition, constructor, or primitive reference"
                              | Ty -> Bool
reacOrStateT (Ty -> Bool) -> Ty -> Bool
forall a b. (a -> b) -> a -> b
$ Exp -> Ty
typeOf Exp
a = Exp -> m ()
tailOk Exp
a
                              | Bool
otherwise               = Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
a)
                                    TyConId
"ANF: a computed argument (must be let-bound)"

            atom :: Annote -> Text -> Exp -> m ()
            atom :: Annote -> TyConId -> Exp -> m ()
atom Annote
an TyConId
what Exp
e = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Exp -> Bool
atomOk Exp
e) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"ANF: " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
what TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" is not an atom"

            atomOk :: Exp -> Bool
            atomOk :: Exp -> Bool
atomOk = Exp -> Bool
isAtom

checkDefn' :: MonadError AstError m => Env -> Defn -> m ()
checkDefn' :: forall (m :: * -> *). MonadError AstError m => Env -> Defn -> m ()
checkDefn' Env
env (Defn Annote
an Id
x [Id]
ps Exp
body Maybe DefnAttr
_ Maybe SpecOrigin
_) = do
      let Sig [TyVar]
tvs Ty
sigT = Id -> Sig
idSig Id
x
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Env -> LintMode
envMode Env
env LintMode -> LintMode -> Bool
forall a. Ord a => a -> a -> Bool
>= LintMode
LintMono) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
tvs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
            (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"definition " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
x TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" has a polymorphic signature (mono mode)"
      let env' :: Env
env' = Env
env { envTVs = Map.fromList [ (tvUniq v, v) | v <- tvs ] }
      Env -> Annote -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTy Env
env' Annote
an Ty
sigT
      let ([Ty]
doms, Ty
res) = Ty -> ([Ty], Ty)
flattenArrow Ty
sigT
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Id] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Id]
ps Uniq -> Uniq -> Bool
forall a. Ord a => a -> a -> Bool
> [Ty] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Ty]
doms) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
            (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"definition " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
x TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" has more parameters than its signature has arrows"
      (Id -> Ty -> m ()) -> [Id] -> [Ty] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (Env -> Annote -> Id -> Id -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Id -> Id -> Ty -> m ()
checkParam Env
env' Annote
an Id
x) [Id]
ps [Ty]
doms
      Env -> Exp -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> Ty -> m ()
checkAgainst ((Id -> Env -> Env) -> Env -> [Id] -> Env
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Id -> Env -> Env
bindVar Env
env' [Id]
ps) Exp
body (Ty -> m ()) -> Ty -> m ()
forall a b. (a -> b) -> a -> b
$ (Ty -> Ty -> Ty) -> Ty -> [Ty] -> Ty
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Annote -> Ty -> Ty -> Ty
Arrow Annote
an) Ty
res ([Ty] -> Ty) -> [Ty] -> Ty
forall a b. (a -> b) -> a -> b
$ Uniq -> [Ty] -> [Ty]
forall a. Uniq -> [a] -> [a]
drop ([Id] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Id]
ps) [Ty]
doms
      where checkParam :: MonadError AstError m => Env -> Annote -> Id -> Id -> Ty -> m ()
            checkParam :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Id -> Id -> Ty -> m ()
checkParam Env
env' Annote
an' Id
f Id
p Ty
dom = do
                  Env -> Annote -> TyConId -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> TyConId -> Id -> m ()
checkValueBinder Env
env' Annote
an' TyConId
"parameter" Id
p
                  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Ty -> Ty -> Bool
tyEq (Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
p) Ty
dom) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an'
                        (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"parameter " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
p TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" of " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
f
                        TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
": type does not match the signature's arrow prefix (expected " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
dom TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
")"

---
--- Local binders.
---

-- | Rules common to every local binder: a monomorphic signature (§3.2) over
--   a well-scoped (and, in mono mode, closed) type.
checkLocalBinder :: MonadError AstError m => Env -> Annote -> Text -> Id -> m ()
checkLocalBinder :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> TyConId -> Id -> m ()
checkLocalBinder Env
env Annote
an TyConId
what Id
x = do
      let Sig [TyVar]
tvs Ty
t = Id -> Sig
idSig Id
x
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
tvs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
            (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
what TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
x TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" has a polymorphic signature (local binders are monomorphic)"
      Env -> Annote -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTy Env
env Annote
an Ty
t

-- | A local *value* binder (parameter, lambda\/let\/case\/pattern binder):
--   additionally first-order in mono+ANF mode (higher-order binders
--   survive specialization; the partial evaluator eliminates them before
--   the ANF stage). Join point labels are exempt — a label's signature is
--   its continuation's function type, and a label is not a value.
checkValueBinder :: MonadError AstError m => Env -> Annote -> Text -> Id -> m ()
checkValueBinder :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> TyConId -> Id -> m ()
checkValueBinder Env
env Annote
an TyConId
what Id
x = do
      Env -> Annote -> TyConId -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> TyConId -> Id -> m ()
checkLocalBinder Env
env Annote
an TyConId
what Id
x
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Env -> LintMode
envMode Env
env LintMode -> LintMode -> Bool
forall a. Ord a => a -> a -> Bool
>= LintMode
LintMonoANF Bool -> Bool -> Bool
&& Ty -> Bool
hasArrow (Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
x)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
            (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
what TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
x TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" has a function type (higher-order binders are not representable past the ANF stage)"
      Env -> Annote -> TyConId -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> TyConId -> Ty -> m ()
checkRepr Env
env Annote
an (TyConId
what TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
x) (Ty -> m ()) -> Ty -> m ()
forall a b. (a -> b) -> a -> b
$ Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
x

-- | Representability at a fixed bit width, when the environment carries
--   the representable closure ('envRepr': the machine level).
checkRepr :: MonadError AstError m => Env -> Annote -> Text -> Ty -> m ()
checkRepr :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> TyConId -> Ty -> m ()
checkRepr Env
env Annote
an TyConId
what Ty
t = case Env -> Maybe (Ty -> Either TyConId Natural)
envRepr Env
env of
      Just Ty -> Either TyConId Natural
sizeOf | Left TyConId
e <- Ty -> Either TyConId Natural
sizeOf Ty
t -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
            (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
what TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" is not representable at a fixed bit width (" TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
e TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
")"
      Maybe (Ty -> Either TyConId Natural)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

---
--- Expressions (doc/eidos.md §4.2): synthesis with all checks inline.
---

-- | Check an expression and return its type — the located, monadic twin of
--   'ReWire.Eidos.Types.typeOf'.
checkExp :: MonadError AstError m => Env -> Exp -> m Ty
checkExp :: forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Ty
checkExp Env
env = \ case
      e :: Exp
e@App {}           -> Env -> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Ty
checkSpine Env
env Exp
e
      Var Annote
an Id
x           -> do
            xB <- Env -> Annote -> Id -> m Id
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Id -> m Id
lookupVar Env
env Annote
an Id
x
            unless (null $ sigTVs $ idSig xB) $ failAt an
                  $ "unsaturated reference to polymorphic " <> prettyPrint x
                  <> " (type arguments must saturate the quantifier list)"
            pure $ sigTy $ idSig xB
      Con Annote
an Ty
t TyConId
c         -> do
            Env -> Annote -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTy Env
env Annote
an Ty
t
            Env -> Annote -> Ty -> TyConId -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> TyConId -> m ()
checkCon Env
env Annote
an Ty
t TyConId
c
            Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
t
      Prim Annote
an Ty
t Builtin
b        -> do
            Env -> Annote -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTy Env
env Annote
an Ty
t
            case Builtin -> Maybe Sig
builtinSig Builtin
b of
                  Just Sig
sig | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Sig -> Ty -> Bool
matchesSig Sig
sig Ty
t -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                        (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"primitive rwPrim" TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Builtin -> TyConId
forall a. TextShow a => a -> TyConId
showt Builtin
b TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" at a type that does not instantiate its signature"
                        TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
"\n      expected an instance of: " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Sig -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Sig
sig
                        TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
"\n      but the occurrence has:  " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
t
                  Maybe Sig
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
t
      LitInt Annote
an Ty
t Integer
n      -> do
            Env -> Annote -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTy Env
env Annote
an Ty
t
            Env -> Annote -> Ty -> Integer -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> Integer -> m ()
checkLitInt Env
env Annote
an Ty
t Integer
n
            Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
t
      LitStr Annote
an TyConId
_        -> Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty -> m Ty) -> Ty -> m Ty
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> Ty
TyCon Annote
an TyConId
"String"
      LitList Annote
an Ty
t [Exp]
es    -> do
            Env -> Annote -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTy Env
env Annote
an Ty
t
            case Ty -> Maybe Ty
dstListTy Ty
t of
                  Just Ty
et -> (Exp -> m ()) -> [Exp] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ Exp
e -> Env -> Exp -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> Ty -> m ()
checkAgainst (Env -> Env
nonTail Env
env) Exp
e Ty
et) [Exp]
es
                  Maybe Ty
Nothing -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"list literal at a non-list type: " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
t
            Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
t
      LitVec Annote
an Ty
t [Exp]
es     -> do
            Env -> Annote -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTy Env
env Annote
an Ty
t
            case Ty -> (Ty, [Ty])
flattenTyApp (Ty -> (Ty, [Ty])) -> Ty -> (Ty, [Ty])
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
natNorm Ty
t of
                  (TyCon Annote
_ TyConId
"Vec", [Ty
n, Ty
et]) -> do
                        (Exp -> m ()) -> [Exp] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ Exp
e -> Env -> Exp -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> Ty -> m ()
checkAgainst (Env -> Env
nonTail Env
env) Exp
e Ty
et) [Exp]
es
                        case Ty -> Maybe Natural
evalNat Ty
n of
                              Just Natural
k  -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Natural
k Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Uniq -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Exp] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Exp]
es)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                                    (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"vector literal has " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Uniq -> TyConId
forall a. TextShow a => a -> TyConId
showt ([Exp] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Exp]
es) TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" elements but type " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
t
                              Maybe Natural
Nothing -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- open length: mono mode rejects the type instead.
                  (Ty, [Ty])
_ -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"vector literal at a non-Vec type: " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
t
            Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
t
      Lam Annote
an Id
x Exp
e         -> do
            Env -> Annote -> TyConId -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> TyConId -> Id -> m ()
checkValueBinder Env
env Annote
an TyConId
"lambda parameter" Id
x
            Annote -> Ty -> Ty -> Ty
Arrow Annote
an (Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
x) (Ty -> Ty) -> m Ty -> m Ty
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Ty
checkExp (Id -> Env -> Env
bindVar Id
x (Env -> Env) -> Env -> Env
forall a b. (a -> b) -> a -> b
$ Env -> Env
nonTail Env
env) Exp
e
      Let Annote
an Bind
b Exp
e         -> Env -> Annote -> Bind -> Exp -> m Ty
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Bind -> Exp -> m Ty
checkLet Env
env Annote
an Bind
b Exp
e
      Jump Annote
an JoinId
j [Exp]
es       -> Env -> Annote -> JoinId -> [Exp] -> m Ty
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> JoinId -> [Exp] -> m Ty
checkJump Env
env Annote
an JoinId
j [Exp]
es
      Case Annote
an Ty
t Exp
e Id
x [Alt]
alts -> Env -> Annote -> Ty -> Exp -> Id -> [Alt] -> m Ty
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> Exp -> Id -> [Alt] -> m Ty
checkCase Env
env Annote
an Ty
t Exp
e Id
x [Alt]
alts

-- | Check an expression against an expected type: synthesize and compare
--   after 'natNorm'.
checkAgainst :: MonadError AstError m => Env -> Exp -> Ty -> m ()
checkAgainst :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> Ty -> m ()
checkAgainst Env
env Exp
e Ty
t = do
      t' <- Env -> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Ty
checkExp Env
env Exp
e
      unless (tyEq t t') $ failAt (ann e)
            $ "expression has type " <> prettyPrint t' <> " but " <> prettyPrint t <> " is expected"

-- | The spine discipline (§4.2): type arguments only on 'Var' heads, in
--   prefix position, saturating the head's quantifier list; then one arrow
--   peeled per term argument, each argument checking against its domain.
checkSpine :: forall m. MonadError AstError m => Env -> Exp -> m Ty
checkSpine :: forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Ty
checkSpine Env
env Exp
e = do
      let (Exp
h, [Arg]
args)  = Exp -> (Exp, [Arg])
flattenApp Exp
e
          ([Arg]
tas, [Arg]
eas) = (Arg -> Bool) -> [Arg] -> ([Arg], [Arg])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Arg -> Bool
isTArg [Arg]
args
          tys :: [Ty]
tys        = [ Ty
t | TArg Ty
t <- [Arg]
tas ]
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Arg -> Bool) -> [Arg] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Arg -> Bool
isTArg [Arg]
eas) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
e) TyConId
"type arguments must form a prefix of the application spine"
      (Ty -> m ()) -> [Ty] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Env -> Annote -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTy Env
env (Annote -> Ty -> m ()) -> Annote -> Ty -> m ()
forall a b. (a -> b) -> a -> b
$ Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
e) [Ty]
tys
      ht <- case Exp
h of
            Var Annote
an Id
x | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Ty] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ty]
tys -> do
                  xB <- Env -> Annote -> Id -> m Id
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Id -> m Id
lookupVar Env
env Annote
an Id
x
                  let sig = Id -> Sig
idSig Id
xB
                  unless (length (sigTVs sig) == length tys) $ failAt an
                        $ prettyPrint x <> " expects " <> showt (length $ sigTVs sig)
                        <> " type arguments, applied to " <> showt (length tys)
                  pure $ instantiate sig tys
            Exp
_ | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Ty] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ty]
tys        -> Annote -> TyConId -> m Ty
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
e) TyConId
"type argument applied to a non-variable head"
              | Bool
otherwise             -> Env -> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Ty
checkExp (Env -> Env
nonTail Env
env) Exp
h
      foldM app ht eas
      where app :: Ty -> Arg -> m Ty
            app :: Ty -> Arg -> m Ty
app Ty
t = \ case
                  EArg Exp
a -> do
                        ta <- Env -> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Ty
checkExp (Env -> Env
nonTail Env
env) Exp
a
                        case t of
                              Arrow Annote
_ Ty
dom Ty
cod -> do
                                    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Ty -> Ty -> Bool
tyEq Ty
dom Ty
ta) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
a)
                                          (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"argument has type " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
ta
                                          TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" but the function expects " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
dom
                                    Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
cod
                              Ty
_               -> Annote -> TyConId -> m Ty
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
a)
                                    (TyConId -> m Ty) -> TyConId -> m Ty
forall a b. (a -> b) -> a -> b
$ TyConId
"term argument applied to a non-arrow (head type " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
t TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
")"
                  TArg Ty
_ -> Annote -> TyConId -> m Ty
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt (Exp -> Annote
forall a. Annotated a => a -> Annote
ann Exp
e) TyConId
"type arguments must form a prefix of the application spine"

            isTArg :: Arg -> Bool
            isTArg :: Arg -> Bool
isTArg = \ case
                  TArg Ty
_ -> Bool
True
                  Arg
_      -> Bool
False

-- | A 'Var' occurrence: bound in scope, with the binder's signature (§4.4).
--   Returns the binder.
lookupVar :: MonadError AstError m => Env -> Annote -> Id -> m Id
lookupVar :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Id -> m Id
lookupVar Env
env Annote
an Id
x = case Uniq -> HashMap Uniq Id -> Maybe Id
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup (Id -> Uniq
idUniq Id
x) (HashMap Uniq Id -> Maybe Id) -> HashMap Uniq Id -> Maybe Id
forall a b. (a -> b) -> a -> b
$ Env -> HashMap Uniq Id
envScope Env
env of
      Just Id
xB -> Annote -> Id -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Annote -> Id -> Id -> m ()
checkOccSig Annote
an Id
x Id
xB m () -> m Id -> m Id
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Id -> m Id
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Id
xB
      Maybe Id
Nothing
            | Uniq -> HashMap Uniq JoinDef -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
Map.member (Id -> Uniq
idUniq Id
x) (HashMap Uniq JoinDef -> Bool) -> HashMap Uniq JoinDef -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> HashMap Uniq JoinDef
envJoins Env
env -> Annote -> TyConId -> m Id
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                  (TyConId -> m Id) -> TyConId -> m Id
forall a b. (a -> b) -> a -> b
$ TyConId
"join point " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
x TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" used as a value (labels may only be jump targets)"
            | Bool
otherwise                            -> Annote -> TyConId -> m Id
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an (TyConId -> m Id) -> TyConId -> m Id
forall a b. (a -> b) -> a -> b
$ TyConId
"unbound variable: " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
x

-- | An occurrence's signature equals its binder's: the same quantified
--   variables (uniques and kinds) over 'natNorm'-structurally equal types.
checkOccSig :: MonadError AstError m => Annote -> Id -> Id -> m ()
checkOccSig :: forall (m :: * -> *).
MonadError AstError m =>
Annote -> Id -> Id -> m ()
checkOccSig Annote
an Id
occ Id
bnd = do
      let Sig [TyVar]
tvs Ty
t   = Id -> Sig
idSig Id
occ
          Sig [TyVar]
tvs' Ty
t' = Id -> Sig
idSig Id
bnd
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TyVar]
tvs [TyVar] -> [TyVar] -> Bool
forall a. Eq a => a -> a -> Bool
== [TyVar]
tvs' Bool -> Bool -> Bool
&& (TyVar -> Kind) -> [TyVar] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> Kind
tvKind [TyVar]
tvs [Kind] -> [Kind] -> Bool
forall a. Eq a => a -> a -> Bool
== (TyVar -> Kind) -> [TyVar] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> Kind
tvKind [TyVar]
tvs' Bool -> Bool -> Bool
&& Ty -> Ty -> Bool
tyEq Ty
t Ty
t') (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
            (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"occurrence of " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
occ TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" carries signature " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Sig -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint (Id -> Sig
idSig Id
occ)
            TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" but its binder carries " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Sig -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint (Id -> Sig
idSig Id
bnd)

-- | A 'Con' occurrence's carried type instantiates its signature: the
--   instantiation is read off the carried type's result by first-order
--   matching against @T as@ (§3.6), then the whole type must agree.
checkCon :: MonadError AstError m => Env -> Annote -> Ty -> DataConId -> m ()
checkCon :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> TyConId -> m ()
checkCon Env
env Annote
an Ty
t TyConId
c = do
      (tcon, sig) <- Env -> Annote -> TyConId -> m (TyConId, Sig)
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> TyConId -> m (TyConId, Sig)
lookupCon Env
env Annote
an TyConId
c
      let (_, res) = flattenArrow t
      fields      <- dconFieldTys an c tcon sig res
      unless (tyEq t $ foldr (Arrow an) res fields) $ failAt an
            $ "constructor " <> c <> " at type " <> prettyPrint t
            <> " does not instantiate its signature " <> prettyPrint sig

lookupCon :: MonadError AstError m => Env -> Annote -> DataConId -> m (TyConId, Sig)
lookupCon :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> TyConId -> m (TyConId, Sig)
lookupCon Env
env Annote
an TyConId
c = m (TyConId, Sig)
-> ((TyConId, Sig) -> m (TyConId, Sig))
-> Maybe (TyConId, Sig)
-> m (TyConId, Sig)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Annote -> TyConId -> m (TyConId, Sig)
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an (TyConId -> m (TyConId, Sig)) -> TyConId -> m (TyConId, Sig)
forall a b. (a -> b) -> a -> b
$ TyConId
"unknown data constructor: " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
c) (TyConId, Sig) -> m (TyConId, Sig)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (TyConId, Sig) -> m (TyConId, Sig))
-> Maybe (TyConId, Sig) -> m (TyConId, Sig)
forall a b. (a -> b) -> a -> b
$ TyConId -> HashMap TyConId (TyConId, Sig) -> Maybe (TyConId, Sig)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup TyConId
c (HashMap TyConId (TyConId, Sig) -> Maybe (TyConId, Sig))
-> HashMap TyConId (TyConId, Sig) -> Maybe (TyConId, Sig)
forall a b. (a -> b) -> a -> b
$ Env -> HashMap TyConId (TyConId, Sig)
envCons Env
env

-- | The instantiated field types of a constructor at a fully-applied
--   datatype type @T ts@ (the scrutinee's type, or a 'Con' occurrence's
--   result type).
dconFieldTys :: MonadError AstError m => Annote -> DataConId -> TyConId -> Sig -> Ty -> m [Ty]
dconFieldTys :: forall (m :: * -> *).
MonadError AstError m =>
Annote -> TyConId -> TyConId -> Sig -> Ty -> m [Ty]
dconFieldTys Annote
an TyConId
c TyConId
tcon (Sig [TyVar]
tvs Ty
sigT) Ty
t = case Ty -> (Ty, [Ty])
flattenTyApp (Ty -> (Ty, [Ty])) -> Ty -> (Ty, [Ty])
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
natNorm Ty
t of
      (TyCon Annote
_ TyConId
t', [Ty]
args) | TyConId
t' TyConId -> TyConId -> Bool
forall a. Eq a => a -> a -> Bool
== TyConId
tcon ->
            if [Ty] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Ty]
args Uniq -> Uniq -> Bool
forall a. Eq a => a -> a -> Bool
== [TyVar] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [TyVar]
tvs
                  then [Ty] -> m [Ty]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Ty] -> m [Ty]) -> [Ty] -> m [Ty]
forall a b. (a -> b) -> a -> b
$ (Ty -> Ty) -> [Ty] -> [Ty]
forall a b. (a -> b) -> [a] -> [b]
map (HashMap TyVar Ty -> Ty -> Ty
substTv (HashMap TyVar Ty -> Ty -> Ty) -> HashMap TyVar Ty -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ [(TyVar, Ty)] -> HashMap TyVar Ty
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList ([(TyVar, Ty)] -> HashMap TyVar Ty)
-> [(TyVar, Ty)] -> HashMap TyVar Ty
forall a b. (a -> b) -> a -> b
$ [TyVar] -> [Ty] -> [(TyVar, Ty)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyVar]
tvs [Ty]
args) ([Ty] -> [Ty]) -> [Ty] -> [Ty]
forall a b. (a -> b) -> a -> b
$ ([Ty], Ty) -> [Ty]
forall a b. (a, b) -> a
fst (([Ty], Ty) -> [Ty]) -> ([Ty], Ty) -> [Ty]
forall a b. (a -> b) -> a -> b
$ Ty -> ([Ty], Ty)
flattenArrow Ty
sigT
                  else Annote -> TyConId -> m [Ty]
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an (TyConId -> m [Ty]) -> TyConId -> m [Ty]
forall a b. (a -> b) -> a -> b
$ TyConId
"constructor " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
c TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
": datatype " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
tcon
                        TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" applied to " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Uniq -> TyConId
forall a. TextShow a => a -> TyConId
showt ([Ty] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Ty]
args) TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" arguments (expected " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Uniq -> TyConId
forall a. TextShow a => a -> TyConId
showt ([TyVar] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [TyVar]
tvs) TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
")"
      (Ty, [Ty])
_ -> Annote -> TyConId -> m [Ty]
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an (TyConId -> m [Ty]) -> TyConId -> m [Ty]
forall a b. (a -> b) -> a -> b
$ TyConId
"constructor " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
c TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" of datatype " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
tcon TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" used at incompatible type " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
t

---
--- Bindings and the join point discipline (doc/eidos.md §3.4, §4.2).
---

checkLet :: MonadError AstError m => Env -> Annote -> Bind -> Exp -> m Ty
checkLet :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Bind -> Exp -> m Ty
checkLet Env
env Annote
an Bind
b Exp
body = case Bind
b of
      NonRec Id
x Exp
e  -> do
            Env -> Annote -> TyConId -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> TyConId -> Id -> m ()
checkValueBinder Env
env Annote
an TyConId
"let binder" Id
x
            Env -> Exp -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> Ty -> m ()
checkAgainst (Env -> Env
nonTail Env
env) Exp
e (Ty -> m ()) -> Ty -> m ()
forall a b. (a -> b) -> a -> b
$ Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
x
            Env -> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Ty
checkExp (Id -> Env -> Env
bindVar Id
x Env
env) Exp
body
      Rec [(Id, Exp)]
bs      -> do
            ((Id, Exp) -> m ()) -> [(Id, Exp)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Env -> Annote -> TyConId -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> TyConId -> Id -> m ()
checkValueBinder Env
env Annote
an TyConId
"recursive let binder" (Id -> m ()) -> ((Id, Exp) -> Id) -> (Id, Exp) -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, Exp) -> Id
forall a b. (a, b) -> a
fst) [(Id, Exp)]
bs
            let env' :: Env
env' = ((Id, Exp) -> Env -> Env) -> Env -> [(Id, Exp)] -> Env
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Id -> Env -> Env
bindVar (Id -> Env -> Env) -> ((Id, Exp) -> Id) -> (Id, Exp) -> Env -> Env
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, Exp) -> Id
forall a b. (a, b) -> a
fst) Env
env [(Id, Exp)]
bs
            ((Id, Exp) -> m ()) -> [(Id, Exp)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Id
x, Exp
e) -> Env -> Exp -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> Ty -> m ()
checkAgainst (Env -> Env
nonTail Env
env') Exp
e (Ty -> m ()) -> Ty -> m ()
forall a b. (a -> b) -> a -> b
$ Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
x) [(Id, Exp)]
bs
            Env -> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Ty
checkExp Env
env' Exp
body
      Join JoinId
j [Id]
xs Exp
e -> do
            let x :: Id
x = JoinId -> Id
jpId JoinId
j
            Env -> Annote -> TyConId -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> TyConId -> Id -> m ()
checkLocalBinder Env
env Annote
an TyConId
"join point" Id
x
            (Id -> m ()) -> [Id] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Env -> Annote -> TyConId -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> TyConId -> Id -> m ()
checkValueBinder Env
env Annote
an TyConId
"join point parameter") [Id]
xs
            Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Id] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Id]
xs Uniq -> Uniq -> Bool
forall a. Eq a => a -> a -> Bool
== JoinId -> Uniq
jpArity JoinId
j) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                  (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"join point " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
x TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" declares arity " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Uniq -> TyConId
forall a. TextShow a => a -> TyConId
showt (JoinId -> Uniq
jpArity JoinId
j)
                  TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" but binds " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Uniq -> TyConId
forall a. TextShow a => a -> TyConId
showt ([Id] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Id]
xs) TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" parameters"
            let ([Ty]
doms, Ty
res) = Ty -> ([Ty], Ty)
flattenArrow (Ty -> ([Ty], Ty)) -> Ty -> ([Ty], Ty)
forall a b. (a -> b) -> a -> b
$ Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
x
            Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Ty] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Ty]
doms Uniq -> Uniq -> Bool
forall a. Ord a => a -> a -> Bool
>= JoinId -> Uniq
jpArity JoinId
j) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                  (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"join point " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
x TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
": signature has fewer arrows than its arity"
            let ptys :: [Ty]
ptys  = Uniq -> [Ty] -> [Ty]
forall a. Uniq -> [a] -> [a]
take (JoinId -> Uniq
jpArity JoinId
j) [Ty]
doms
                resTy :: Ty
resTy = (Ty -> Ty -> Ty) -> Ty -> [Ty] -> Ty
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Annote -> Ty -> Ty -> Ty
Arrow Annote
an) Ty
res ([Ty] -> Ty) -> [Ty] -> Ty
forall a b. (a -> b) -> a -> b
$ Uniq -> [Ty] -> [Ty]
forall a. Uniq -> [a] -> [a]
drop (JoinId -> Uniq
jpArity JoinId
j) [Ty]
doms
                jd :: JoinDef
jd    = JoinId -> [Ty] -> Ty -> JoinDef
JoinDef JoinId
j [Ty]
ptys Ty
resTy
            (Id -> Ty -> m ()) -> [Id] -> [Ty] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (\ Id
p Ty
pt -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Ty -> Ty -> Bool
tyEq (Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
p) Ty
pt) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                        (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"join point parameter " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
p
                        TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
": type does not match the join point's signature (expected " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
pt TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
")")
                  [Id]
xs [Ty]
ptys
            -- The join body and the scope check against the same type (the
            -- join's result is the scope's result). Outer joins remain
            -- jumpable from the body's tail (it is transitively a tail of
            -- their scopes); the join itself is not (no recursion).
            Env -> Exp -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> Ty -> m ()
checkAgainst ((Id -> Env -> Env) -> Env -> [Id] -> Env
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Id -> Env -> Env
bindVar (Id -> JoinDef -> Env -> Env
scopeJoin Id
x JoinDef
jd Env
env) [Id]
xs) Exp
e Ty
resTy
            tb <- Env -> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Ty
checkExp (Id -> JoinDef -> Env -> Env
bindJoin Id
x JoinDef
jd Env
env) Exp
body
            unless (tyEq tb resTy) $ failAt an
                  $ "the scope of join point " <> prettyPrint x <> " has type " <> prettyPrint tb
                  <> " but the join point returns " <> prettyPrint resTy
            pure tb

-- | A jump: to a join point bound in an enclosing let, from tail position
--   of that join's scope, saturating its arity, each argument checking
--   against the corresponding parameter type.
checkJump :: MonadError AstError m => Env -> Annote -> JoinId -> [Exp] -> m Ty
checkJump :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> JoinId -> [Exp] -> m Ty
checkJump Env
env Annote
an JoinId
j [Exp]
args = case Uniq -> HashMap Uniq JoinDef -> Maybe JoinDef
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup (Id -> Uniq
idUniq (Id -> Uniq) -> Id -> Uniq
forall a b. (a -> b) -> a -> b
$ JoinId -> Id
jpId JoinId
j) (HashMap Uniq JoinDef -> Maybe JoinDef)
-> HashMap Uniq JoinDef -> Maybe JoinDef
forall a b. (a -> b) -> a -> b
$ Env -> HashMap Uniq JoinDef
envJoins Env
env of
      Just (JoinDef JoinId
jB [Ty]
ptys Ty
res) -> do
            Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Id -> Uniq
idUniq (JoinId -> Id
jpId JoinId
j) Uniq -> HashSet Uniq -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` Env -> HashSet Uniq
envTail Env
env) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                  (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"jump to join point " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint (JoinId -> Id
jpId JoinId
j)
                  TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" outside the tail of its scope (jumps are tail-only, and join points are not recursive)"
            Annote -> Id -> Id -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Annote -> Id -> Id -> m ()
checkOccSig Annote
an (JoinId -> Id
jpId JoinId
j) (Id -> m ()) -> Id -> m ()
forall a b. (a -> b) -> a -> b
$ JoinId -> Id
jpId JoinId
jB
            Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (JoinId -> Uniq
jpArity JoinId
j Uniq -> Uniq -> Bool
forall a. Eq a => a -> a -> Bool
== JoinId -> Uniq
jpArity JoinId
jB) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                  (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"jump to " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint (JoinId -> Id
jpId JoinId
j) TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" carries arity " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Uniq -> TyConId
forall a. TextShow a => a -> TyConId
showt (JoinId -> Uniq
jpArity JoinId
j)
                  TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" but the join point declares " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Uniq -> TyConId
forall a. TextShow a => a -> TyConId
showt (JoinId -> Uniq
jpArity JoinId
jB)
            Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Exp] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Exp]
args Uniq -> Uniq -> Bool
forall a. Eq a => a -> a -> Bool
== JoinId -> Uniq
jpArity JoinId
jB) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                  (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"jump to " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint (JoinId -> Id
jpId JoinId
j) TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" supplies " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Uniq -> TyConId
forall a. TextShow a => a -> TyConId
showt ([Exp] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Exp]
args)
                  TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" arguments (arity " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Uniq -> TyConId
forall a. TextShow a => a -> TyConId
showt (JoinId -> Uniq
jpArity JoinId
jB) TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
")"
            (Exp -> Ty -> m ()) -> [Exp] -> [Ty] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (Env -> Exp -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> Ty -> m ()
checkAgainst (Env -> Exp -> Ty -> m ()) -> Env -> Exp -> Ty -> m ()
forall a b. (a -> b) -> a -> b
$ Env -> Env
nonTail Env
env) [Exp]
args [Ty]
ptys
            Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
res
      Maybe JoinDef
Nothing
            | Uniq -> HashMap Uniq Id -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
Map.member (Id -> Uniq
idUniq (Id -> Uniq) -> Id -> Uniq
forall a b. (a -> b) -> a -> b
$ JoinId -> Id
jpId JoinId
j) (HashMap Uniq Id -> Bool) -> HashMap Uniq Id -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> HashMap Uniq Id
envScope Env
env -> Annote -> TyConId -> m Ty
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                  (TyConId -> m Ty) -> TyConId -> m Ty
forall a b. (a -> b) -> a -> b
$ TyConId
"jump target " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint (JoinId -> Id
jpId JoinId
j) TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" is a value binder, not a join point"
            | Bool
otherwise                                   -> Annote -> TyConId -> m Ty
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                  (TyConId -> m Ty) -> TyConId -> m Ty
forall a b. (a -> b) -> a -> b
$ TyConId
"jump to unbound join point " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint (JoinId -> Id
jpId JoinId
j) TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" (labels do not escape their scope)"

---
--- Case expressions (doc/eidos.md §4.2).
---

checkCase :: MonadError AstError m => Env -> Annote -> Ty -> Exp -> Id -> [Alt] -> m Ty
checkCase :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> Exp -> Id -> [Alt] -> m Ty
checkCase Env
env Annote
an Ty
t Exp
scrut Id
x [Alt]
alts = do
      Env -> Annote -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTy Env
env Annote
an Ty
t
      ts <- Env -> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Ty
checkExp (Env -> Env
nonTail Env
env) Exp
scrut
      checkValueBinder env an "case binder" x
      unless (tyEq (sigTy $ idSig x) ts) $ failAt an
            $ "case binder " <> prettyPrint x <> " has type " <> prettyPrint (sigTy $ idSig x)
            <> " but the scrutinee has type " <> prettyPrint ts
      when (null alts) $ failAt an "case expression with no alternatives"
      case [ an' | Alt an' DefaultAlt _ _ <- drop 1 alts ] of
            Annote
an' : [Annote]
_ -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an' TyConId
"the default case alternative must come first"
            []      -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      checkDistinct [ (c, an', "case alternative for constructor " <> c) | Alt an' (DataAlt c) _ _ <- alts ]
      checkDistinct [ (n, an', "case alternative for literal " <> showt n) | Alt an' (LitAlt n) _ _ <- alts ]
      mapM_ (checkAlt (bindVar x env) t ts) alts
      pure t

-- | One alternative: fields bound at the constructor's instantiated field
--   types; the body (a tail position) checks against the carried result
--   type.
checkAlt :: MonadError AstError m => Env -> Ty -> Ty -> Alt -> m ()
checkAlt :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Ty -> Ty -> Alt -> m ()
checkAlt Env
env Ty
t Ty
ts (Alt Annote
an AltCon
con [Id]
xs Exp
body) = case AltCon
con of
      AltCon
DefaultAlt -> do
            Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Id] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
xs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an TyConId
"default case alternative binds fields"
            Env -> Exp -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> Ty -> m ()
checkAgainst Env
env Exp
body Ty
t
      LitAlt Integer
n   -> do
            Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Id] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
xs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an TyConId
"literal case alternative binds fields"
            case Ty -> LitRep
litRep Ty
ts of
                  LitRep
RepBad -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"literal case alternative on a scrutinee of type " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
ts
                        TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" (must be Integer, a bit vector, or Finite)"
                  LitRep
rep    -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Env -> LintMode
envMode Env
env LintMode -> LintMode -> Bool
forall a. Ord a => a -> a -> Bool
>= LintMode
LintMono) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LitRep -> Integer -> Bool
fitsRep LitRep
rep Integer
n) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                        (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"literal " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Integer -> TyConId
forall a. TextShow a => a -> TyConId
showt Integer
n TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" is not representable at the scrutinee type " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
ts
            Env -> Exp -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Exp -> Ty -> m ()
checkAgainst Env
env Exp
body Ty
t
      DataAlt TyConId
c  -> do
            (tcon, sig) <- Env -> Annote -> TyConId -> m (TyConId, Sig)
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> TyConId -> m (TyConId, Sig)
lookupCon Env
env Annote
an TyConId
c
            fields      <- dconFieldTys an c tcon sig ts
            unless (length xs == length fields) $ failAt an
                  $ "case alternative for " <> c <> " binds " <> showt (length xs)
                  <> " fields (the constructor has " <> showt (length fields) <> ")"
            mapM_ (checkValueBinder env an "pattern binder") xs
            zipWithM_ (\ Id
p Ty
ft -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Ty -> Ty -> Bool
tyEq (Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
p) Ty
ft) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                        (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"pattern binder " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Id -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Id
p
                        TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
": type does not match the constructor's field type " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
ft)
                  xs fields
            checkAgainst (foldr bindVar env xs) body t

---
--- Integer literals (doc/eidos.md §4.2): representability, mono mode only
--- (widths may be open in poly mode).
---

data LitRep = RepInteger | RepBits !Natural | RepFinite !Natural | RepOpen | RepBad

litRep :: Ty -> LitRep
litRep :: Ty -> LitRep
litRep Ty
t = case Ty -> (Ty, [Ty])
flattenTyApp (Ty -> (Ty, [Ty])) -> Ty -> (Ty, [Ty])
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
natNorm Ty
t of
      (TyCon Annote
_ TyConId
"Integer", [])              -> LitRep
RepInteger
      (TyCon Annote
_ TyConId
"Vec", [Ty
w, TyCon Annote
_ TyConId
"Bool"]) -> LitRep -> (Natural -> LitRep) -> Maybe Natural -> LitRep
forall b a. b -> (a -> b) -> Maybe a -> b
maybe LitRep
RepOpen Natural -> LitRep
RepBits (Maybe Natural -> LitRep) -> Maybe Natural -> LitRep
forall a b. (a -> b) -> a -> b
$ Ty -> Maybe Natural
evalNat Ty
w
      (TyCon Annote
_ TyConId
"Finite", [Ty
w])              -> LitRep -> (Natural -> LitRep) -> Maybe Natural -> LitRep
forall b a. b -> (a -> b) -> Maybe a -> b
maybe LitRep
RepOpen Natural -> LitRep
RepFinite (Maybe Natural -> LitRep) -> Maybe Natural -> LitRep
forall a b. (a -> b) -> a -> b
$ Ty -> Maybe Natural
evalNat Ty
w
      (Ty, [Ty])
_                                    -> LitRep
RepBad

fitsRep :: LitRep -> Integer -> Bool
fitsRep :: LitRep -> Integer -> Bool
fitsRep LitRep
rep Integer
n = case LitRep
rep of
      LitRep
RepInteger  -> Bool
True
      LitRep
RepOpen     -> Bool
True -- unreachable in mono mode (types are nat-closed).
      RepBits Natural
w   | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0    -> Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2 Integer -> Natural -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Natural
w
                  | Bool
otherwise -> Natural
w Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
0 Bool -> Bool -> Bool
&& Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Integer
forall a. Num a => a -> a
negate (Integer
2 Integer -> Natural -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Natural
w Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1))
      RepFinite Natural
w -> Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 Bool -> Bool -> Bool
&& Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
w
      LitRep
RepBad      -> Bool
False

checkLitInt :: MonadError AstError m => Env -> Annote -> Ty -> Integer -> m ()
checkLitInt :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> Integer -> m ()
checkLitInt Env
env Annote
an Ty
t Integer
n = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Env -> LintMode
envMode Env
env LintMode -> LintMode -> Bool
forall a. Ord a => a -> a -> Bool
>= LintMode
LintMono) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ case Ty -> LitRep
litRep Ty
t of
      LitRep
RepBad -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"integer literal at unrepresentable type " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
t
            TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" (must be Integer, a bit vector, or Finite)"
      LitRep
rep    -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LitRep -> Integer -> Bool
fitsRep LitRep
rep Integer
n) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
            (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"literal " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Integer -> TyConId
forall a. TextShow a => a -> TyConId
showt Integer
n TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" is not representable at type " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
t

---
--- Types.
---

-- | Scoping (every type variable bound, at its binder's kind) plus, in
--   mono mode, closedness; at the machine level ('envBanReactive'), the
--   reactive types are out of the grammar entirely (doc/eidos.md §4.1).
checkTy :: MonadError AstError m => Env -> Annote -> Ty -> m ()
checkTy :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTy Env
env Annote
an Ty
t = do
      Env -> Annote -> Ty -> m ()
forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTyScope Env
env Annote
an Ty
t
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Env -> LintMode
envMode Env
env LintMode -> LintMode -> Bool
forall a. Ord a => a -> a -> Bool
>= LintMode
LintMono) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> Ty -> m ()
forall (m :: * -> *). MonadError AstError m => Annote -> Ty -> m ()
checkClosed Annote
an (Ty -> m ()) -> Ty -> m ()
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
natNorm Ty
t
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Env -> Bool
envBanReactive Env
env Bool -> Bool -> Bool
&& Ty -> Bool
reacOrStateT Ty
t) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
            (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"reactive type " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> Ty -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint Ty
t TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" in Synolon (purification has retired ReacT/StateT/Identity)"

checkTyScope :: MonadError AstError m => Env -> Annote -> Ty -> m ()
checkTyScope :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Annote -> Ty -> m ()
checkTyScope Env
env Annote
an = Ty -> m ()
forall (m :: * -> *). MonadError AstError m => Ty -> m ()
go
      where go :: MonadError AstError m => Ty -> m ()
            go :: forall (m :: * -> *). MonadError AstError m => Ty -> m ()
go = \ case
                  TyVarT Annote
_ TyVar
v    -> case Uniq -> HashMap Uniq TyVar -> Maybe TyVar
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup (TyVar -> Uniq
tvUniq TyVar
v) (HashMap Uniq TyVar -> Maybe TyVar)
-> HashMap Uniq TyVar -> Maybe TyVar
forall a b. (a -> b) -> a -> b
$ Env -> HashMap Uniq TyVar
envTVs Env
env of
                        Just TyVar
v' | TyVar -> Kind
tvKind TyVar
v' Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Kind
tvKind TyVar
v -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                                | Bool
otherwise             -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                              (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"type variable " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyVar -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint TyVar
v TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
": occurrence kind does not match its binder's"
                        Maybe TyVar
Nothing                         -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"unbound type variable: " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyVar -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint TyVar
v
                  TyApp Annote
_ Ty
t1 Ty
t2 -> Ty -> m ()
forall (m :: * -> *). MonadError AstError m => Ty -> m ()
go Ty
t1 m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Ty -> m ()
forall (m :: * -> *). MonadError AstError m => Ty -> m ()
go Ty
t2
                  Arrow Annote
_ Ty
t1 Ty
t2 -> Ty -> m ()
forall (m :: * -> *). MonadError AstError m => Ty -> m ()
go Ty
t1 m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Ty -> m ()
forall (m :: * -> *). MonadError AstError m => Ty -> m ()
go Ty
t2
                  Ty
_             -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | On a 'natNorm'-normalized type: no type variables, and no residual
--   type-level arithmetic (every nat-closed subterm has already been folded
--   to a literal, so any surviving arithmetic constructor is open).
checkClosed :: MonadError AstError m => Annote -> Ty -> m ()
checkClosed :: forall (m :: * -> *). MonadError AstError m => Annote -> Ty -> m ()
checkClosed Annote
an = Ty -> m ()
forall (m :: * -> *). MonadError AstError m => Ty -> m ()
go
      where go :: MonadError AstError m => Ty -> m ()
            go :: forall (m :: * -> *). MonadError AstError m => Ty -> m ()
go = \ case
                  TyVarT Annote
_ TyVar
v    -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an (TyConId -> m ()) -> TyConId -> m ()
forall a b. (a -> b) -> a -> b
$ TyConId
"type variable " TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyVar -> TyConId
forall a. Pretty a => a -> TyConId
prettyPrint TyVar
v TyConId -> TyConId -> TyConId
forall a. Semigroup a => a -> a -> a
<> TyConId
" in mono mode (types must be closed)"
                  TyCon Annote
_ TyConId
c     | TyConId
c TyConId -> [TyConId] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([TyConId
"+", TyConId
"-", TyConId
"*"] :: [Text]) -> Annote -> TyConId -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> TyConId -> m a
failAt Annote
an
                        TyConId
"type-level arithmetic does not evaluate to a literal (types must be nat-closed in mono mode)"
                  TyApp Annote
_ Ty
t1 Ty
t2 -> Ty -> m ()
forall (m :: * -> *). MonadError AstError m => Ty -> m ()
go Ty
t1 m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Ty -> m ()
forall (m :: * -> *). MonadError AstError m => Ty -> m ()
go Ty
t2
                  Arrow Annote
_ Ty
t1 Ty
t2 -> Ty -> m ()
forall (m :: * -> *). MonadError AstError m => Ty -> m ()
go Ty
t1 m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Ty -> m ()
forall (m :: * -> *). MonadError AstError m => Ty -> m ()
go Ty
t2
                  Ty
_             -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | The list type constructor applied to an element type. Both the
--   bridge's spelling (@[_]@) and the source spelling (@[]@, for
--   hand-written Eidos) are accepted here.
dstListTy :: Ty -> Maybe Ty
dstListTy :: Ty -> Maybe Ty
dstListTy = \ case
      TyApp Annote
_ (TyCon Annote
_ TyConId
c) Ty
et | TyConId
c TyConId -> TyConId -> Bool
forall a. Eq a => a -> a -> Bool
== TyConId
"[_]" Bool -> Bool -> Bool
|| TyConId
c TyConId -> TyConId -> Bool
forall a. Eq a => a -> a -> Bool
== TyConId
"[]" -> Ty -> Maybe Ty
forall a. a -> Maybe a
Just Ty
et
      Ty
_                                                -> Maybe Ty
forall a. Maybe a
Nothing