{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedStrings #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Parsing types in the Swarm language.
module Swarm.Language.Parser.Type (
  parsePolytype,
  parseType,
  parseTypeMolecule,
  parseTypeAtom,
  parseTyCon,
) where

import Control.Monad.Combinators (many)
import Control.Monad.Combinators.Expr (Operator (..), makeExprParser)
import Data.Fix (Fix (..), foldFix)
import Data.List.Extra (enumerate)
import Data.Maybe (fromMaybe)
import Swarm.Language.Parser.Core (Parser)
import Swarm.Language.Parser.Lex (
  braces,
  brackets,
  parens,
  reserved,
  reservedCS,
  symbol,
  tyName,
  tyVar,
 )
import Swarm.Language.Parser.Record (parseRecord)
import Swarm.Language.Types
import Text.Megaparsec (choice, optional, some, (<|>))

-- | Parse a Swarm language polytype, which starts with an optional
--   quanitifation (@forall@ followed by one or more variables and a
--   period) followed by a type.  Note that anything accepted by
--   'parseType' is also accepted by 'parsePolytype'.
parsePolytype :: Parser RawPolytype
parsePolytype :: Parser RawPolytype
parsePolytype =
  [Var] -> Type -> RawPolytype
forall t. [Var] -> t -> Poly 'Unquantified t
mkPoly ([Var] -> Type -> RawPolytype)
-> (Maybe [Var] -> [Var]) -> Maybe [Var] -> Type -> RawPolytype
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Var] -> Maybe [Var] -> [Var]
forall a. a -> Maybe a -> a
fromMaybe []
    (Maybe [Var] -> Type -> RawPolytype)
-> ReaderT
     ParserConfig (StateT WSState (Parsec Void Var)) (Maybe [Var])
-> ReaderT
     ParserConfig
     (StateT WSState (Parsec Void Var))
     (Type -> RawPolytype)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) [Var]
-> ReaderT
     ParserConfig (StateT WSState (Parsec Void Var)) (Maybe [Var])
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional ((Var -> Parser ()
reserved Var
"forall" Parser () -> Parser () -> Parser ()
forall a.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Var -> Parser ()
reserved Var
"∀") Parser ()
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) [Var]
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) [Var]
forall a b.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) [Var]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
tyVar ReaderT ParserConfig (StateT WSState (Parsec Void Var)) [Var]
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) [Var]
forall a b.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Var -> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
symbol Var
".")
    ReaderT
  ParserConfig
  (StateT WSState (Parsec Void Var))
  (Type -> RawPolytype)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> Parser RawPolytype
forall a b.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) (a -> b)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
parseType

-- | Parse a Swarm language (mono)type.
parseType :: Parser Type
parseType :: ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
parseType = ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> [[Operator
       (ReaderT ParserConfig (StateT WSState (Parsec Void Var))) Type]]
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
makeExprParser ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
parseTypeMolecule [[Operator
    (ReaderT ParserConfig (StateT WSState (Parsec Void Var))) Type]]
table
 where
  table :: [[Operator
    (ReaderT ParserConfig (StateT WSState (Parsec Void Var))) Type]]
table =
    [ [ReaderT
  ParserConfig
  (StateT WSState (Parsec Void Var))
  (Type -> Type -> Type)
-> Operator
     (ReaderT ParserConfig (StateT WSState (Parsec Void Var))) Type
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (Type -> Type -> Type
(:*:) (Type -> Type -> Type)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
-> ReaderT
     ParserConfig
     (StateT WSState (Parsec Void Var))
     (Type -> Type -> Type)
forall a b.
a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var -> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
symbol Var
"*")]
    , [ReaderT
  ParserConfig
  (StateT WSState (Parsec Void Var))
  (Type -> Type -> Type)
-> Operator
     (ReaderT ParserConfig (StateT WSState (Parsec Void Var))) Type
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (Type -> Type -> Type
(:+:) (Type -> Type -> Type)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
-> ReaderT
     ParserConfig
     (StateT WSState (Parsec Void Var))
     (Type -> Type -> Type)
forall a b.
a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var -> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
symbol Var
"+")]
    , [ReaderT
  ParserConfig
  (StateT WSState (Parsec Void Var))
  (Type -> Type -> Type)
-> Operator
     (ReaderT ParserConfig (StateT WSState (Parsec Void Var))) Type
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (Type -> Type -> Type
(:->:) (Type -> Type -> Type)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
-> ReaderT
     ParserConfig
     (StateT WSState (Parsec Void Var))
     (Type -> Type -> Type)
forall a b.
a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var -> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
symbol Var
"->")]
    ]

-- | A "type molecule" consists of either a type constructor applied
--   to a chain of type atoms, or just a type atom by itself.  We have
--   to separate this out from parseTypeAtom to deal with the left
--   recursion.
parseTypeMolecule :: Parser Type
parseTypeMolecule :: ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
parseTypeMolecule =
  TyCon -> [Type] -> Type
TyConApp (TyCon -> [Type] -> Type)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
-> ReaderT
     ParserConfig (StateT WSState (Parsec Void Var)) ([Type] -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
parseTyCon ReaderT
  ParserConfig (StateT WSState (Parsec Void Var)) ([Type] -> Type)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) [Type]
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall a b.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) (a -> b)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) [Type]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
parseTypeAtom
    ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall a.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
parseTypeAtom

-- | A "type atom" consists of some atomic type snytax --- type
--   variables, things in brackets of some kind, or a lone type
--   constructor.
parseTypeAtom :: Parser Type
parseTypeAtom :: ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
parseTypeAtom =
  Var -> Type
TyVar (Var -> Type)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
tyVar
    ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall a.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TyCon -> [Type] -> Type
TyConApp (TyCon -> [Type] -> Type)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
-> ReaderT
     ParserConfig (StateT WSState (Parsec Void Var)) ([Type] -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
parseTyCon ReaderT
  ParserConfig (StateT WSState (Parsec Void Var)) ([Type] -> Type)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) [Type]
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall a b.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) (a -> b)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Type]
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) [Type]
forall a.
a -> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall a.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type -> Type
TyDelay (Type -> Type)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall a. Parser a -> Parser a
braces ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
parseType
    ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall a.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Map Var Type -> Type
TyRcd (Map Var Type -> Type)
-> ReaderT
     ParserConfig (StateT WSState (Parsec Void Var)) (Map Var Type)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT
  ParserConfig (StateT WSState (Parsec Void Var)) (Map Var Type)
-> ReaderT
     ParserConfig (StateT WSState (Parsec Void Var)) (Map Var Type)
forall a. Parser a -> Parser a
brackets (ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT WSState (Parsec Void Var)) (Map Var Type)
forall a. Parser a -> Parser (Map Var a)
parseRecord (Var -> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
symbol Var
":" ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall a b.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
parseType))
    ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall a.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Var -> Type -> Type
tyRec (Var -> Type -> Type)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
-> ReaderT
     ParserConfig (StateT WSState (Parsec Void Var)) (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var -> Parser ()
reserved Var
"rec" Parser ()
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
forall a b.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
tyVar) ReaderT
  ParserConfig (StateT WSState (Parsec Void Var)) (Type -> Type)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall a b.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) (a -> b)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Var -> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
symbol Var
"." ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Var
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall a b.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
parseType)
    ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall a.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
forall a. Parser a -> Parser a
parens ReaderT ParserConfig (StateT WSState (Parsec Void Var)) Type
parseType

-- | A type constructor.
parseTyCon :: Parser TyCon
parseTyCon :: ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
parseTyCon = do
  [ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon]
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ((BaseTy
 -> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon)
-> [BaseTy]
-> [ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon]
forall a b. (a -> b) -> [a] -> [b]
map (\BaseTy
b -> BaseTy -> TyCon
TCBase BaseTy
b TyCon
-> Parser ()
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
forall a b.
a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var -> Parser ()
reservedCS (BaseTy -> Var
baseTyName BaseTy
b)) [BaseTy]
forall a. (Enum a, Bounded a) => [a]
enumerate)
    ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
forall a.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TyCon
TCCmd TyCon
-> Parser ()
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
forall a b.
a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var -> Parser ()
reservedCS Var
"Cmd"
    ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
forall a.
ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TDVar -> TyCon
TCUser (TDVar -> TyCon)
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TDVar
-> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TyCon
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT ParserConfig (StateT WSState (Parsec Void Var)) TDVar
tyName

-- | Close over a recursive type, replacing any bound occurrences
--   of its variable in the body with de Bruijn indices.  Note that
--   (1) we don't have to worry about conflicts with type variables
--   bound by a top-level @forall@; since @forall@ must always be at
--   the top level, any @rec@ will necessarily be lexically within the
--   scope of any @forall@ and hence variables bound by @rec@ will
--   shadow any variables bound by a @forall@.  For example, @forall
--   a. a -> (rec a. unit + a)@ is a function from an arbitrary type
--   to a recursive natural number. (2) Any @rec@ contained inside
--   this one will have already been closed over when it was parsed,
--   and its bound variables thus replaced by de Bruijn indices, so
--   neither do we have to worry about being shadowed --- any
--   remaining free occurrences of the variable name in question are
--   indeed references to this @rec@ binder.
tyRec :: Var -> Type -> Type
tyRec :: Var -> Type -> Type
tyRec Var
x = Var -> Type -> Type
TyRec Var
x (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Nat -> Type) -> Nat -> Type
forall a b. (a -> b) -> a -> b
$ Nat
NZ) ((Nat -> Type) -> Type) -> (Type -> Nat -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeF (Nat -> Type) -> Nat -> Type) -> Type -> Nat -> Type
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix TypeF (Nat -> Type) -> Nat -> Type
s
 where
  s :: TypeF (Nat -> Type) -> Nat -> Type
  s :: TypeF (Nat -> Type) -> Nat -> Type
s = \case
    TyRecF Var
y Nat -> Type
ty -> TypeF Type -> Type
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF Type -> Type) -> (Nat -> TypeF Type) -> Nat -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Type -> TypeF Type
forall t. Var -> t -> TypeF t
TyRecF Var
y (Type -> TypeF Type) -> (Nat -> Type) -> Nat -> TypeF Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Type
ty (Nat -> Type) -> (Nat -> Nat) -> Nat -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Nat
NS
    TyVarF Var
orig Var
y
      | Var
x Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
y -> TypeF Type -> Type
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF Type -> Type) -> (Nat -> TypeF Type) -> Nat -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> TypeF Type
forall t. Nat -> TypeF t
TyRecVarF
      | Bool
otherwise -> Type -> Nat -> Type
forall a b. a -> b -> a
const (TypeF Type -> Type
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Var -> Var -> TypeF Type
forall t. Var -> Var -> TypeF t
TyVarF Var
orig Var
y))
    TypeF (Nat -> Type)
fty -> \Nat
i -> TypeF Type -> Type
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (((Nat -> Type) -> Type) -> TypeF (Nat -> Type) -> TypeF Type
forall a b. (a -> b) -> TypeF a -> TypeF b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Nat -> Type) -> Nat -> Type
forall a b. (a -> b) -> a -> b
$ Nat
i) TypeF (Nat -> Type)
fty)