{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Types for the Swarm programming language and related utilities.
module Swarm.Language.Types (
  -- * Basic definitions

  -- ** Base types and type constructors
  BaseTy (..),
  baseTyName,
  TyCon (..),
  Arity (..),
  tcArity,
  Var,

  -- ** Type structure functor
  TypeF (..),

  -- ** Recursive types
  Nat (..),
  natToInt,
  unfoldRec,
  SubstRec (..),

  -- * @Type@
  Type,
  tyVars,
  pattern TyConApp,
  pattern TyBase,
  pattern TyVar,
  pattern TyVoid,
  pattern TyUnit,
  pattern TyInt,
  pattern TyText,
  pattern TyDir,
  pattern TyBool,
  pattern TyActor,
  pattern TyKey,
  pattern (:+:),
  pattern (:*:),
  pattern (:->:),
  pattern TyRcd,
  pattern TyCmd,
  pattern TyDelay,
  pattern TyUser,
  pattern TyRec,

  -- * @UType@
  IntVar (..),
  UType,
  pattern UTyConApp,
  pattern UTyBase,
  pattern UTyVar,
  pattern UTyVoid,
  pattern UTyUnit,
  pattern UTyInt,
  pattern UTyText,
  pattern UTyDir,
  pattern UTyBool,
  pattern UTyActor,
  pattern UTyKey,
  pattern UTySum,
  pattern UTyProd,
  pattern UTyFun,
  pattern UTyRcd,
  pattern UTyCmd,
  pattern UTyDelay,
  pattern UTyUser,
  pattern UTyRec,

  -- ** Utilities
  ucata,
  mkVarName,
  fuvs,

  -- * Polytypes
  Poly (..),
  Polytype,
  pattern PolyUnit,
  UPolytype,

  -- * Contexts
  TCtx,
  UCtx,

  -- * User type definitions
  TydefInfo (..),
  tydefType,
  tydefArity,
  substTydef,
  expandTydef,
  elimTydef,
  TDCtx,

  -- * WHNF
  whnfType,

  -- * The 'WithU' class
  WithU (..),
) where

import Control.Algebra (Has, run)
import Control.Carrier.Reader (runReader)
import Control.Effect.Reader (Reader, ask)
import Control.Lens (makeLenses, view)
import Control.Monad.Free
import Data.Aeson (FromJSON (..), FromJSON1 (..), ToJSON (..), ToJSON1 (..), genericLiftParseJSON, genericLiftToJSON, genericParseJSON, genericToJSON)
import Data.Data (Data)
import Data.Eq.Deriving (deriveEq1)
import Data.Fix
import Data.Foldable (fold)
import Data.Kind qualified
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as M
import Data.Maybe (fromMaybe)
import Data.Ord.Deriving (deriveOrd1)
import Data.Set (Set)
import Data.Set qualified as S
import Data.String (IsString (..))
import Data.Text (Text)
import Data.Text qualified as T
import GHC.Generics (Generic, Generic1)
import Swarm.Language.Context (Ctx, Var)
import Swarm.Language.Context qualified as Ctx
import Swarm.Util (parens, showT)
import Swarm.Util.JSON (optionsMinimize, optionsUnwrapUnary)
import Text.Show.Deriving (deriveShow1)
import Witch

------------------------------------------------------------
-- Base types
------------------------------------------------------------

-- | Base types.
data BaseTy
  = -- | The void type, with no inhabitants.
    BVoid
  | -- | The unit type, with a single inhabitant.
    BUnit
  | -- | Signed, arbitrary-size integers.
    BInt
  | -- | Unicode strings.
    BText
  | -- | Directions.
    BDir
  | -- | Booleans.
    BBool
  | -- | "Actors", i.e. anything that can do stuff. Internally, these
    --   are all just "robots", but we give them a more generic
    --   in-game name because they could represent other things like
    --   aliens, animals, seeds, ...
    BActor
  | -- | Keys, i.e. things that can be pressed on the keyboard
    BKey
  deriving (BaseTy -> BaseTy -> Bool
(BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool) -> Eq BaseTy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BaseTy -> BaseTy -> Bool
== :: BaseTy -> BaseTy -> Bool
$c/= :: BaseTy -> BaseTy -> Bool
/= :: BaseTy -> BaseTy -> Bool
Eq, Eq BaseTy
Eq BaseTy =>
(BaseTy -> BaseTy -> Ordering)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> BaseTy)
-> (BaseTy -> BaseTy -> BaseTy)
-> Ord BaseTy
BaseTy -> BaseTy -> Bool
BaseTy -> BaseTy -> Ordering
BaseTy -> BaseTy -> BaseTy
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 :: BaseTy -> BaseTy -> Ordering
compare :: BaseTy -> BaseTy -> Ordering
$c< :: BaseTy -> BaseTy -> Bool
< :: BaseTy -> BaseTy -> Bool
$c<= :: BaseTy -> BaseTy -> Bool
<= :: BaseTy -> BaseTy -> Bool
$c> :: BaseTy -> BaseTy -> Bool
> :: BaseTy -> BaseTy -> Bool
$c>= :: BaseTy -> BaseTy -> Bool
>= :: BaseTy -> BaseTy -> Bool
$cmax :: BaseTy -> BaseTy -> BaseTy
max :: BaseTy -> BaseTy -> BaseTy
$cmin :: BaseTy -> BaseTy -> BaseTy
min :: BaseTy -> BaseTy -> BaseTy
Ord, Int -> BaseTy -> ShowS
[BaseTy] -> ShowS
BaseTy -> [Char]
(Int -> BaseTy -> ShowS)
-> (BaseTy -> [Char]) -> ([BaseTy] -> ShowS) -> Show BaseTy
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BaseTy -> ShowS
showsPrec :: Int -> BaseTy -> ShowS
$cshow :: BaseTy -> [Char]
show :: BaseTy -> [Char]
$cshowList :: [BaseTy] -> ShowS
showList :: [BaseTy] -> ShowS
Show, BaseTy
BaseTy -> BaseTy -> Bounded BaseTy
forall a. a -> a -> Bounded a
$cminBound :: BaseTy
minBound :: BaseTy
$cmaxBound :: BaseTy
maxBound :: BaseTy
Bounded, Int -> BaseTy
BaseTy -> Int
BaseTy -> [BaseTy]
BaseTy -> BaseTy
BaseTy -> BaseTy -> [BaseTy]
BaseTy -> BaseTy -> BaseTy -> [BaseTy]
(BaseTy -> BaseTy)
-> (BaseTy -> BaseTy)
-> (Int -> BaseTy)
-> (BaseTy -> Int)
-> (BaseTy -> [BaseTy])
-> (BaseTy -> BaseTy -> [BaseTy])
-> (BaseTy -> BaseTy -> [BaseTy])
-> (BaseTy -> BaseTy -> BaseTy -> [BaseTy])
-> Enum BaseTy
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: BaseTy -> BaseTy
succ :: BaseTy -> BaseTy
$cpred :: BaseTy -> BaseTy
pred :: BaseTy -> BaseTy
$ctoEnum :: Int -> BaseTy
toEnum :: Int -> BaseTy
$cfromEnum :: BaseTy -> Int
fromEnum :: BaseTy -> Int
$cenumFrom :: BaseTy -> [BaseTy]
enumFrom :: BaseTy -> [BaseTy]
$cenumFromThen :: BaseTy -> BaseTy -> [BaseTy]
enumFromThen :: BaseTy -> BaseTy -> [BaseTy]
$cenumFromTo :: BaseTy -> BaseTy -> [BaseTy]
enumFromTo :: BaseTy -> BaseTy -> [BaseTy]
$cenumFromThenTo :: BaseTy -> BaseTy -> BaseTy -> [BaseTy]
enumFromThenTo :: BaseTy -> BaseTy -> BaseTy -> [BaseTy]
Enum, Typeable BaseTy
Typeable BaseTy =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> BaseTy -> c BaseTy)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BaseTy)
-> (BaseTy -> Constr)
-> (BaseTy -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BaseTy))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy))
-> ((forall b. Data b => b -> b) -> BaseTy -> BaseTy)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> BaseTy -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> BaseTy -> r)
-> (forall u. (forall d. Data d => d -> u) -> BaseTy -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy)
-> Data BaseTy
BaseTy -> Constr
BaseTy -> DataType
(forall b. Data b => b -> b) -> BaseTy -> BaseTy
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
$ctoConstr :: BaseTy -> Constr
toConstr :: BaseTy -> Constr
$cdataTypeOf :: BaseTy -> DataType
dataTypeOf :: BaseTy -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
$cgmapT :: (forall b. Data b => b -> b) -> BaseTy -> BaseTy
gmapT :: (forall b. Data b => b -> b) -> BaseTy -> BaseTy
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
Data, (forall x. BaseTy -> Rep BaseTy x)
-> (forall x. Rep BaseTy x -> BaseTy) -> Generic BaseTy
forall x. Rep BaseTy x -> BaseTy
forall x. BaseTy -> Rep BaseTy x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BaseTy -> Rep BaseTy x
from :: forall x. BaseTy -> Rep BaseTy x
$cto :: forall x. Rep BaseTy x -> BaseTy
to :: forall x. Rep BaseTy x -> BaseTy
Generic, Maybe BaseTy
Value -> Parser [BaseTy]
Value -> Parser BaseTy
(Value -> Parser BaseTy)
-> (Value -> Parser [BaseTy]) -> Maybe BaseTy -> FromJSON BaseTy
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser BaseTy
parseJSON :: Value -> Parser BaseTy
$cparseJSONList :: Value -> Parser [BaseTy]
parseJSONList :: Value -> Parser [BaseTy]
$comittedField :: Maybe BaseTy
omittedField :: Maybe BaseTy
FromJSON, [BaseTy] -> Value
[BaseTy] -> Encoding
BaseTy -> Bool
BaseTy -> Value
BaseTy -> Encoding
(BaseTy -> Value)
-> (BaseTy -> Encoding)
-> ([BaseTy] -> Value)
-> ([BaseTy] -> Encoding)
-> (BaseTy -> Bool)
-> ToJSON BaseTy
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: BaseTy -> Value
toJSON :: BaseTy -> Value
$ctoEncoding :: BaseTy -> Encoding
toEncoding :: BaseTy -> Encoding
$ctoJSONList :: [BaseTy] -> Value
toJSONList :: [BaseTy] -> Value
$ctoEncodingList :: [BaseTy] -> Encoding
toEncodingList :: [BaseTy] -> Encoding
$comitField :: BaseTy -> Bool
omitField :: BaseTy -> Bool
ToJSON)

baseTyName :: BaseTy -> Text
baseTyName :: BaseTy -> Text
baseTyName = forall target source. From source target => source -> target
into @Text ([Char] -> Text) -> (BaseTy -> [Char]) -> BaseTy -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
1 ShowS -> (BaseTy -> [Char]) -> BaseTy -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseTy -> [Char]
forall a. Show a => a -> [Char]
show

------------------------------------------------------------
-- Type constructors
------------------------------------------------------------

-- | Type constructors.
data TyCon
  = -- | Base types are (nullary) type constructors.
    TCBase BaseTy
  | -- | Command types.
    TCCmd
  | -- | Delayed computations.
    TCDelay
  | -- | Sum types.
    TCSum
  | -- | Product types.
    TCProd
  | -- | Function types.
    TCFun
  | -- | User-defined type constructor.
    TCUser Var
  deriving (TyCon -> TyCon -> Bool
(TyCon -> TyCon -> Bool) -> (TyCon -> TyCon -> Bool) -> Eq TyCon
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TyCon -> TyCon -> Bool
== :: TyCon -> TyCon -> Bool
$c/= :: TyCon -> TyCon -> Bool
/= :: TyCon -> TyCon -> Bool
Eq, Eq TyCon
Eq TyCon =>
(TyCon -> TyCon -> Ordering)
-> (TyCon -> TyCon -> Bool)
-> (TyCon -> TyCon -> Bool)
-> (TyCon -> TyCon -> Bool)
-> (TyCon -> TyCon -> Bool)
-> (TyCon -> TyCon -> TyCon)
-> (TyCon -> TyCon -> TyCon)
-> Ord TyCon
TyCon -> TyCon -> Bool
TyCon -> TyCon -> Ordering
TyCon -> TyCon -> TyCon
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 :: TyCon -> TyCon -> Ordering
compare :: TyCon -> TyCon -> Ordering
$c< :: TyCon -> TyCon -> Bool
< :: TyCon -> TyCon -> Bool
$c<= :: TyCon -> TyCon -> Bool
<= :: TyCon -> TyCon -> Bool
$c> :: TyCon -> TyCon -> Bool
> :: TyCon -> TyCon -> Bool
$c>= :: TyCon -> TyCon -> Bool
>= :: TyCon -> TyCon -> Bool
$cmax :: TyCon -> TyCon -> TyCon
max :: TyCon -> TyCon -> TyCon
$cmin :: TyCon -> TyCon -> TyCon
min :: TyCon -> TyCon -> TyCon
Ord, Int -> TyCon -> ShowS
[TyCon] -> ShowS
TyCon -> [Char]
(Int -> TyCon -> ShowS)
-> (TyCon -> [Char]) -> ([TyCon] -> ShowS) -> Show TyCon
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TyCon -> ShowS
showsPrec :: Int -> TyCon -> ShowS
$cshow :: TyCon -> [Char]
show :: TyCon -> [Char]
$cshowList :: [TyCon] -> ShowS
showList :: [TyCon] -> ShowS
Show, Typeable TyCon
Typeable TyCon =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TyCon -> c TyCon)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TyCon)
-> (TyCon -> Constr)
-> (TyCon -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TyCon))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyCon))
-> ((forall b. Data b => b -> b) -> TyCon -> TyCon)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyCon -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyCon -> r)
-> (forall u. (forall d. Data d => d -> u) -> TyCon -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TyCon -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TyCon -> m TyCon)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TyCon -> m TyCon)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TyCon -> m TyCon)
-> Data TyCon
TyCon -> Constr
TyCon -> DataType
(forall b. Data b => b -> b) -> TyCon -> TyCon
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TyCon -> u
forall u. (forall d. Data d => d -> u) -> TyCon -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyCon -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyCon -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TyCon -> m TyCon
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyCon -> m TyCon
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyCon
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyCon -> c TyCon
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TyCon)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyCon)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyCon -> c TyCon
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyCon -> c TyCon
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyCon
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyCon
$ctoConstr :: TyCon -> Constr
toConstr :: TyCon -> Constr
$cdataTypeOf :: TyCon -> DataType
dataTypeOf :: TyCon -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TyCon)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TyCon)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyCon)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyCon)
$cgmapT :: (forall b. Data b => b -> b) -> TyCon -> TyCon
gmapT :: (forall b. Data b => b -> b) -> TyCon -> TyCon
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyCon -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyCon -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyCon -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyCon -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TyCon -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> TyCon -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TyCon -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TyCon -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TyCon -> m TyCon
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TyCon -> m TyCon
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyCon -> m TyCon
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyCon -> m TyCon
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyCon -> m TyCon
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyCon -> m TyCon
Data, (forall x. TyCon -> Rep TyCon x)
-> (forall x. Rep TyCon x -> TyCon) -> Generic TyCon
forall x. Rep TyCon x -> TyCon
forall x. TyCon -> Rep TyCon x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TyCon -> Rep TyCon x
from :: forall x. TyCon -> Rep TyCon x
$cto :: forall x. Rep TyCon x -> TyCon
to :: forall x. Rep TyCon x -> TyCon
Generic)

instance ToJSON TyCon where
  toJSON :: TyCon -> Value
toJSON = Options -> TyCon -> Value
forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
optionsMinimize

instance FromJSON TyCon where
  parseJSON :: Value -> Parser TyCon
parseJSON = Options -> Value -> Parser TyCon
forall a.
(Generic a, GFromJSON Zero (Rep a)) =>
Options -> Value -> Parser a
genericParseJSON Options
optionsMinimize

-- | The arity of a type, /i.e./ the number of type parameters it
--   expects.
newtype Arity = Arity {Arity -> Int
getArity :: Int}
  deriving (Arity -> Arity -> Bool
(Arity -> Arity -> Bool) -> (Arity -> Arity -> Bool) -> Eq Arity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Arity -> Arity -> Bool
== :: Arity -> Arity -> Bool
$c/= :: Arity -> Arity -> Bool
/= :: Arity -> Arity -> Bool
Eq, Eq Arity
Eq Arity =>
(Arity -> Arity -> Ordering)
-> (Arity -> Arity -> Bool)
-> (Arity -> Arity -> Bool)
-> (Arity -> Arity -> Bool)
-> (Arity -> Arity -> Bool)
-> (Arity -> Arity -> Arity)
-> (Arity -> Arity -> Arity)
-> Ord Arity
Arity -> Arity -> Bool
Arity -> Arity -> Ordering
Arity -> Arity -> Arity
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 :: Arity -> Arity -> Ordering
compare :: Arity -> Arity -> Ordering
$c< :: Arity -> Arity -> Bool
< :: Arity -> Arity -> Bool
$c<= :: Arity -> Arity -> Bool
<= :: Arity -> Arity -> Bool
$c> :: Arity -> Arity -> Bool
> :: Arity -> Arity -> Bool
$c>= :: Arity -> Arity -> Bool
>= :: Arity -> Arity -> Bool
$cmax :: Arity -> Arity -> Arity
max :: Arity -> Arity -> Arity
$cmin :: Arity -> Arity -> Arity
min :: Arity -> Arity -> Arity
Ord, Int -> Arity -> ShowS
[Arity] -> ShowS
Arity -> [Char]
(Int -> Arity -> ShowS)
-> (Arity -> [Char]) -> ([Arity] -> ShowS) -> Show Arity
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Arity -> ShowS
showsPrec :: Int -> Arity -> ShowS
$cshow :: Arity -> [Char]
show :: Arity -> [Char]
$cshowList :: [Arity] -> ShowS
showList :: [Arity] -> ShowS
Show, (forall x. Arity -> Rep Arity x)
-> (forall x. Rep Arity x -> Arity) -> Generic Arity
forall x. Rep Arity x -> Arity
forall x. Arity -> Rep Arity x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Arity -> Rep Arity x
from :: forall x. Arity -> Rep Arity x
$cto :: forall x. Rep Arity x -> Arity
to :: forall x. Rep Arity x -> Arity
Generic, Typeable Arity
Typeable Arity =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Arity -> c Arity)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Arity)
-> (Arity -> Constr)
-> (Arity -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Arity))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Arity))
-> ((forall b. Data b => b -> b) -> Arity -> Arity)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Arity -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Arity -> r)
-> (forall u. (forall d. Data d => d -> u) -> Arity -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Arity -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Arity -> m Arity)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Arity -> m Arity)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Arity -> m Arity)
-> Data Arity
Arity -> Constr
Arity -> DataType
(forall b. Data b => b -> b) -> Arity -> Arity
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Arity -> u
forall u. (forall d. Data d => d -> u) -> Arity -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Arity -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Arity -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Arity -> m Arity
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Arity -> m Arity
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Arity
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Arity -> c Arity
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Arity)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Arity)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Arity -> c Arity
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Arity -> c Arity
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Arity
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Arity
$ctoConstr :: Arity -> Constr
toConstr :: Arity -> Constr
$cdataTypeOf :: Arity -> DataType
dataTypeOf :: Arity -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Arity)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Arity)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Arity)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Arity)
$cgmapT :: (forall b. Data b => b -> b) -> Arity -> Arity
gmapT :: (forall b. Data b => b -> b) -> Arity -> Arity
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Arity -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Arity -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Arity -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Arity -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Arity -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Arity -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Arity -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Arity -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Arity -> m Arity
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Arity -> m Arity
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Arity -> m Arity
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Arity -> m Arity
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Arity -> m Arity
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Arity -> m Arity
Data)

instance ToJSON Arity where
  toJSON :: Arity -> Value
toJSON = Options -> Arity -> Value
forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
optionsUnwrapUnary

instance FromJSON Arity where
  parseJSON :: Value -> Parser Arity
parseJSON = Options -> Value -> Parser Arity
forall a.
(Generic a, GFromJSON Zero (Rep a)) =>
Options -> Value -> Parser a
genericParseJSON Options
optionsUnwrapUnary

------------------------------------------------------------
-- Types
------------------------------------------------------------

-- | Peano naturals, for use as de Bruijn indices in recursive types.
data Nat where
  NZ :: Nat
  NS :: Nat -> Nat
  deriving (Nat -> Nat -> Bool
(Nat -> Nat -> Bool) -> (Nat -> Nat -> Bool) -> Eq Nat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Nat -> Nat -> Bool
== :: Nat -> Nat -> Bool
$c/= :: Nat -> Nat -> Bool
/= :: Nat -> Nat -> Bool
Eq, Eq Nat
Eq Nat =>
(Nat -> Nat -> Ordering)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Nat)
-> (Nat -> Nat -> Nat)
-> Ord Nat
Nat -> Nat -> Bool
Nat -> Nat -> Ordering
Nat -> Nat -> Nat
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 :: Nat -> Nat -> Ordering
compare :: Nat -> Nat -> Ordering
$c< :: Nat -> Nat -> Bool
< :: Nat -> Nat -> Bool
$c<= :: Nat -> Nat -> Bool
<= :: Nat -> Nat -> Bool
$c> :: Nat -> Nat -> Bool
> :: Nat -> Nat -> Bool
$c>= :: Nat -> Nat -> Bool
>= :: Nat -> Nat -> Bool
$cmax :: Nat -> Nat -> Nat
max :: Nat -> Nat -> Nat
$cmin :: Nat -> Nat -> Nat
min :: Nat -> Nat -> Nat
Ord, Int -> Nat -> ShowS
[Nat] -> ShowS
Nat -> [Char]
(Int -> Nat -> ShowS)
-> (Nat -> [Char]) -> ([Nat] -> ShowS) -> Show Nat
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Nat -> ShowS
showsPrec :: Int -> Nat -> ShowS
$cshow :: Nat -> [Char]
show :: Nat -> [Char]
$cshowList :: [Nat] -> ShowS
showList :: [Nat] -> ShowS
Show, Typeable Nat
Typeable Nat =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Nat -> c Nat)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Nat)
-> (Nat -> Constr)
-> (Nat -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Nat))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat))
-> ((forall b. Data b => b -> b) -> Nat -> Nat)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r)
-> (forall u. (forall d. Data d => d -> u) -> Nat -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Nat -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Nat -> m Nat)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Nat -> m Nat)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Nat -> m Nat)
-> Data Nat
Nat -> Constr
Nat -> DataType
(forall b. Data b => b -> b) -> Nat -> Nat
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Nat -> u
forall u. (forall d. Data d => d -> u) -> Nat -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Nat
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Nat -> c Nat
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Nat)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Nat -> c Nat
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Nat -> c Nat
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Nat
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Nat
$ctoConstr :: Nat -> Constr
toConstr :: Nat -> Constr
$cdataTypeOf :: Nat -> DataType
dataTypeOf :: Nat -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Nat)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Nat)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat)
$cgmapT :: (forall b. Data b => b -> b) -> Nat -> Nat
gmapT :: (forall b. Data b => b -> b) -> Nat -> Nat
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Nat -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Nat -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Nat -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Nat -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
Data, (forall x. Nat -> Rep Nat x)
-> (forall x. Rep Nat x -> Nat) -> Generic Nat
forall x. Rep Nat x -> Nat
forall x. Nat -> Rep Nat x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Nat -> Rep Nat x
from :: forall x. Nat -> Rep Nat x
$cto :: forall x. Rep Nat x -> Nat
to :: forall x. Rep Nat x -> Nat
Generic, Maybe Nat
Value -> Parser [Nat]
Value -> Parser Nat
(Value -> Parser Nat)
-> (Value -> Parser [Nat]) -> Maybe Nat -> FromJSON Nat
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser Nat
parseJSON :: Value -> Parser Nat
$cparseJSONList :: Value -> Parser [Nat]
parseJSONList :: Value -> Parser [Nat]
$comittedField :: Maybe Nat
omittedField :: Maybe Nat
FromJSON, [Nat] -> Value
[Nat] -> Encoding
Nat -> Bool
Nat -> Value
Nat -> Encoding
(Nat -> Value)
-> (Nat -> Encoding)
-> ([Nat] -> Value)
-> ([Nat] -> Encoding)
-> (Nat -> Bool)
-> ToJSON Nat
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: Nat -> Value
toJSON :: Nat -> Value
$ctoEncoding :: Nat -> Encoding
toEncoding :: Nat -> Encoding
$ctoJSONList :: [Nat] -> Value
toJSONList :: [Nat] -> Value
$ctoEncodingList :: [Nat] -> Encoding
toEncodingList :: [Nat] -> Encoding
$comitField :: Nat -> Bool
omitField :: Nat -> Bool
ToJSON)

natToInt :: Nat -> Int
natToInt :: Nat -> Int
natToInt Nat
NZ = Int
0
natToInt (NS Nat
n) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Nat -> Int
natToInt Nat
n

-- | A "structure functor" encoding the shape of type expressions.
--   Actual types are then represented by taking a fixed point of this
--   functor.  We represent types in this way, via a "two-level type",
--   so that we can easily use generic recursion schemes to implement
--   things like substitution.
data TypeF t
  = -- | A type constructor applied to some type arguments. For now,
    --   all type constructor applications are required to be fully
    --   saturated (higher kinds are not supported), so we just
    --   directly store a list of all arguments (as opposed to
    --   iterating binary application).
    TyConF TyCon [t]
  | -- | A type variable.
    TyVarF Var
  | -- | Record type.
    TyRcdF (Map Var t)
  | -- | A recursive type variable bound by an enclosing Rec,
    --   represented by a de Bruijn index.
    TyRecVarF Nat
  | -- | Recursive type.  The variable is just a suggestion for a name to use
    --   when pretty-printing; the actual bound variables are represented
    --   via de Bruijn indices.
    TyRecF Var t
  deriving (Int -> TypeF t -> ShowS
[TypeF t] -> ShowS
TypeF t -> [Char]
(Int -> TypeF t -> ShowS)
-> (TypeF t -> [Char]) -> ([TypeF t] -> ShowS) -> Show (TypeF t)
forall t. Show t => Int -> TypeF t -> ShowS
forall t. Show t => [TypeF t] -> ShowS
forall t. Show t => TypeF t -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> TypeF t -> ShowS
showsPrec :: Int -> TypeF t -> ShowS
$cshow :: forall t. Show t => TypeF t -> [Char]
show :: TypeF t -> [Char]
$cshowList :: forall t. Show t => [TypeF t] -> ShowS
showList :: [TypeF t] -> ShowS
Show, TypeF t -> TypeF t -> Bool
(TypeF t -> TypeF t -> Bool)
-> (TypeF t -> TypeF t -> Bool) -> Eq (TypeF t)
forall t. Eq t => TypeF t -> TypeF t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall t. Eq t => TypeF t -> TypeF t -> Bool
== :: TypeF t -> TypeF t -> Bool
$c/= :: forall t. Eq t => TypeF t -> TypeF t -> Bool
/= :: TypeF t -> TypeF t -> Bool
Eq, Eq (TypeF t)
Eq (TypeF t) =>
(TypeF t -> TypeF t -> Ordering)
-> (TypeF t -> TypeF t -> Bool)
-> (TypeF t -> TypeF t -> Bool)
-> (TypeF t -> TypeF t -> Bool)
-> (TypeF t -> TypeF t -> Bool)
-> (TypeF t -> TypeF t -> TypeF t)
-> (TypeF t -> TypeF t -> TypeF t)
-> Ord (TypeF t)
TypeF t -> TypeF t -> Bool
TypeF t -> TypeF t -> Ordering
TypeF t -> TypeF t -> TypeF t
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
forall t. Ord t => Eq (TypeF t)
forall t. Ord t => TypeF t -> TypeF t -> Bool
forall t. Ord t => TypeF t -> TypeF t -> Ordering
forall t. Ord t => TypeF t -> TypeF t -> TypeF t
$ccompare :: forall t. Ord t => TypeF t -> TypeF t -> Ordering
compare :: TypeF t -> TypeF t -> Ordering
$c< :: forall t. Ord t => TypeF t -> TypeF t -> Bool
< :: TypeF t -> TypeF t -> Bool
$c<= :: forall t. Ord t => TypeF t -> TypeF t -> Bool
<= :: TypeF t -> TypeF t -> Bool
$c> :: forall t. Ord t => TypeF t -> TypeF t -> Bool
> :: TypeF t -> TypeF t -> Bool
$c>= :: forall t. Ord t => TypeF t -> TypeF t -> Bool
>= :: TypeF t -> TypeF t -> Bool
$cmax :: forall t. Ord t => TypeF t -> TypeF t -> TypeF t
max :: TypeF t -> TypeF t -> TypeF t
$cmin :: forall t. Ord t => TypeF t -> TypeF t -> TypeF t
min :: TypeF t -> TypeF t -> TypeF t
Ord, (forall a b. (a -> b) -> TypeF a -> TypeF b)
-> (forall a b. a -> TypeF b -> TypeF a) -> Functor TypeF
forall a b. a -> TypeF b -> TypeF a
forall a b. (a -> b) -> TypeF a -> TypeF b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> TypeF a -> TypeF b
fmap :: forall a b. (a -> b) -> TypeF a -> TypeF b
$c<$ :: forall a b. a -> TypeF b -> TypeF a
<$ :: forall a b. a -> TypeF b -> TypeF a
Functor, (forall m. Monoid m => TypeF m -> m)
-> (forall m a. Monoid m => (a -> m) -> TypeF a -> m)
-> (forall m a. Monoid m => (a -> m) -> TypeF a -> m)
-> (forall a b. (a -> b -> b) -> b -> TypeF a -> b)
-> (forall a b. (a -> b -> b) -> b -> TypeF a -> b)
-> (forall b a. (b -> a -> b) -> b -> TypeF a -> b)
-> (forall b a. (b -> a -> b) -> b -> TypeF a -> b)
-> (forall a. (a -> a -> a) -> TypeF a -> a)
-> (forall a. (a -> a -> a) -> TypeF a -> a)
-> (forall a. TypeF a -> [a])
-> (forall a. TypeF a -> Bool)
-> (forall a. TypeF a -> Int)
-> (forall a. Eq a => a -> TypeF a -> Bool)
-> (forall a. Ord a => TypeF a -> a)
-> (forall a. Ord a => TypeF a -> a)
-> (forall a. Num a => TypeF a -> a)
-> (forall a. Num a => TypeF a -> a)
-> Foldable TypeF
forall a. Eq a => a -> TypeF a -> Bool
forall a. Num a => TypeF a -> a
forall a. Ord a => TypeF a -> a
forall m. Monoid m => TypeF m -> m
forall a. TypeF a -> Bool
forall a. TypeF a -> Int
forall a. TypeF a -> [a]
forall a. (a -> a -> a) -> TypeF a -> a
forall m a. Monoid m => (a -> m) -> TypeF a -> m
forall b a. (b -> a -> b) -> b -> TypeF a -> b
forall a b. (a -> b -> b) -> b -> TypeF a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => TypeF m -> m
fold :: forall m. Monoid m => TypeF m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> TypeF a -> a
foldr1 :: forall a. (a -> a -> a) -> TypeF a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TypeF a -> a
foldl1 :: forall a. (a -> a -> a) -> TypeF a -> a
$ctoList :: forall a. TypeF a -> [a]
toList :: forall a. TypeF a -> [a]
$cnull :: forall a. TypeF a -> Bool
null :: forall a. TypeF a -> Bool
$clength :: forall a. TypeF a -> Int
length :: forall a. TypeF a -> Int
$celem :: forall a. Eq a => a -> TypeF a -> Bool
elem :: forall a. Eq a => a -> TypeF a -> Bool
$cmaximum :: forall a. Ord a => TypeF a -> a
maximum :: forall a. Ord a => TypeF a -> a
$cminimum :: forall a. Ord a => TypeF a -> a
minimum :: forall a. Ord a => TypeF a -> a
$csum :: forall a. Num a => TypeF a -> a
sum :: forall a. Num a => TypeF a -> a
$cproduct :: forall a. Num a => TypeF a -> a
product :: forall a. Num a => TypeF a -> a
Foldable, Functor TypeF
Foldable TypeF
(Functor TypeF, Foldable TypeF) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> TypeF a -> f (TypeF b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    TypeF (f a) -> f (TypeF a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TypeF a -> m (TypeF b))
-> (forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a))
-> Traversable TypeF
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeF a -> f (TypeF b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeF a -> f (TypeF b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeF a -> f (TypeF b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
sequenceA :: forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
$csequence :: forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
sequence :: forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
Traversable, (forall x. TypeF t -> Rep (TypeF t) x)
-> (forall x. Rep (TypeF t) x -> TypeF t) -> Generic (TypeF t)
forall x. Rep (TypeF t) x -> TypeF t
forall x. TypeF t -> Rep (TypeF t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (TypeF t) x -> TypeF t
forall t x. TypeF t -> Rep (TypeF t) x
$cfrom :: forall t x. TypeF t -> Rep (TypeF t) x
from :: forall x. TypeF t -> Rep (TypeF t) x
$cto :: forall t x. Rep (TypeF t) x -> TypeF t
to :: forall x. Rep (TypeF t) x -> TypeF t
Generic, (forall a. TypeF a -> Rep1 TypeF a)
-> (forall a. Rep1 TypeF a -> TypeF a) -> Generic1 TypeF
forall a. Rep1 TypeF a -> TypeF a
forall a. TypeF a -> Rep1 TypeF a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cfrom1 :: forall a. TypeF a -> Rep1 TypeF a
from1 :: forall a. TypeF a -> Rep1 TypeF a
$cto1 :: forall a. Rep1 TypeF a -> TypeF a
to1 :: forall a. Rep1 TypeF a -> TypeF a
Generic1, Typeable (TypeF t)
Typeable (TypeF t) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TypeF t -> c (TypeF t))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (TypeF t))
-> (TypeF t -> Constr)
-> (TypeF t -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (TypeF t)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TypeF t)))
-> ((forall b. Data b => b -> b) -> TypeF t -> TypeF t)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TypeF t -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TypeF t -> r)
-> (forall u. (forall d. Data d => d -> u) -> TypeF t -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TypeF t -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t))
-> Data (TypeF t)
TypeF t -> Constr
TypeF t -> DataType
(forall b. Data b => b -> b) -> TypeF t -> TypeF t
forall t. Data t => Typeable (TypeF t)
forall t. Data t => TypeF t -> Constr
forall t. Data t => TypeF t -> DataType
forall t.
Data t =>
(forall b. Data b => b -> b) -> TypeF t -> TypeF t
forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> TypeF t -> u
forall t u.
Data t =>
(forall d. Data d => d -> u) -> TypeF t -> [u]
forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TypeF t)
forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeF t -> c (TypeF t)
forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TypeF t))
forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TypeF t))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TypeF t -> u
forall u. (forall d. Data d => d -> u) -> TypeF t -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TypeF t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeF t -> c (TypeF t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (TypeF t))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TypeF t))
$cgfoldl :: forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeF t -> c (TypeF t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeF t -> c (TypeF t)
$cgunfold :: forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TypeF t)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TypeF t)
$ctoConstr :: forall t. Data t => TypeF t -> Constr
toConstr :: TypeF t -> Constr
$cdataTypeOf :: forall t. Data t => TypeF t -> DataType
dataTypeOf :: TypeF t -> DataType
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TypeF t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (TypeF t))
$cdataCast2 :: forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TypeF t))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TypeF t))
$cgmapT :: forall t.
Data t =>
(forall b. Data b => b -> b) -> TypeF t -> TypeF t
gmapT :: (forall b. Data b => b -> b) -> TypeF t -> TypeF t
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
$cgmapQr :: forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
$cgmapQ :: forall t u.
Data t =>
(forall d. Data d => d -> u) -> TypeF t -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> TypeF t -> [u]
$cgmapQi :: forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> TypeF t -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TypeF t -> u
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
$cgmapMp :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
$cgmapMo :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
Data)

deriveEq1 ''TypeF
deriveOrd1 ''TypeF
deriveShow1 ''TypeF

instance ToJSON1 TypeF where
  liftToJSON :: forall a.
(a -> Bool) -> (a -> Value) -> ([a] -> Value) -> TypeF a -> Value
liftToJSON = Options
-> (a -> Bool)
-> (a -> Value)
-> ([a] -> Value)
-> TypeF a
-> Value
forall (f :: * -> *) a.
(Generic1 f, GToJSON' Value One (Rep1 f)) =>
Options
-> (a -> Bool) -> (a -> Value) -> ([a] -> Value) -> f a -> Value
genericLiftToJSON Options
optionsMinimize

instance FromJSON1 TypeF where
  liftParseJSON :: forall a.
Maybe a
-> (Value -> Parser a)
-> (Value -> Parser [a])
-> Value
-> Parser (TypeF a)
liftParseJSON = Options
-> Maybe a
-> (Value -> Parser a)
-> (Value -> Parser [a])
-> Value
-> Parser (TypeF a)
forall (f :: * -> *) a.
(Generic1 f, GFromJSON One (Rep1 f)) =>
Options
-> Maybe a
-> (Value -> Parser a)
-> (Value -> Parser [a])
-> Value
-> Parser (f a)
genericLiftParseJSON Options
optionsMinimize

-- | @Type@ is now defined as the fixed point of 'TypeF'.  It would be
--   annoying to manually apply and match against 'Fix' constructors
--   everywhere, so we provide pattern synonyms that allow us to work
--   with 'Type' as if it were defined in a directly recursive way.
type Type = Fix TypeF

-- | Get all the type variables contained in a 'Type'.
tyVars :: Type -> Set Var
tyVars :: Type -> Set Text
tyVars = (TypeF (Set Text) -> Set Text) -> Type -> Set Text
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix (\case TyVarF Text
x -> Text -> Set Text
forall a. a -> Set a
S.singleton Text
x; TypeF (Set Text)
f -> TypeF (Set Text) -> Set Text
forall m. Monoid m => TypeF m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold TypeF (Set Text)
f)

newtype IntVar = IntVar Int
  deriving (Int -> IntVar -> ShowS
[IntVar] -> ShowS
IntVar -> [Char]
(Int -> IntVar -> ShowS)
-> (IntVar -> [Char]) -> ([IntVar] -> ShowS) -> Show IntVar
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IntVar -> ShowS
showsPrec :: Int -> IntVar -> ShowS
$cshow :: IntVar -> [Char]
show :: IntVar -> [Char]
$cshowList :: [IntVar] -> ShowS
showList :: [IntVar] -> ShowS
Show, Typeable IntVar
Typeable IntVar =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> IntVar -> c IntVar)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c IntVar)
-> (IntVar -> Constr)
-> (IntVar -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c IntVar))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IntVar))
-> ((forall b. Data b => b -> b) -> IntVar -> IntVar)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> IntVar -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> IntVar -> r)
-> (forall u. (forall d. Data d => d -> u) -> IntVar -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> IntVar -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> IntVar -> m IntVar)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> IntVar -> m IntVar)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> IntVar -> m IntVar)
-> Data IntVar
IntVar -> Constr
IntVar -> DataType
(forall b. Data b => b -> b) -> IntVar -> IntVar
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> IntVar -> u
forall u. (forall d. Data d => d -> u) -> IntVar -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IntVar -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IntVar -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> IntVar -> m IntVar
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IntVar -> m IntVar
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c IntVar
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> IntVar -> c IntVar
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c IntVar)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IntVar)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> IntVar -> c IntVar
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> IntVar -> c IntVar
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c IntVar
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c IntVar
$ctoConstr :: IntVar -> Constr
toConstr :: IntVar -> Constr
$cdataTypeOf :: IntVar -> DataType
dataTypeOf :: IntVar -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c IntVar)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c IntVar)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IntVar)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IntVar)
$cgmapT :: (forall b. Data b => b -> b) -> IntVar -> IntVar
gmapT :: (forall b. Data b => b -> b) -> IntVar -> IntVar
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IntVar -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IntVar -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IntVar -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IntVar -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> IntVar -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> IntVar -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> IntVar -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> IntVar -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> IntVar -> m IntVar
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> IntVar -> m IntVar
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IntVar -> m IntVar
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IntVar -> m IntVar
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IntVar -> m IntVar
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> IntVar -> m IntVar
Data, IntVar -> IntVar -> Bool
(IntVar -> IntVar -> Bool)
-> (IntVar -> IntVar -> Bool) -> Eq IntVar
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IntVar -> IntVar -> Bool
== :: IntVar -> IntVar -> Bool
$c/= :: IntVar -> IntVar -> Bool
/= :: IntVar -> IntVar -> Bool
Eq, Eq IntVar
Eq IntVar =>
(IntVar -> IntVar -> Ordering)
-> (IntVar -> IntVar -> Bool)
-> (IntVar -> IntVar -> Bool)
-> (IntVar -> IntVar -> Bool)
-> (IntVar -> IntVar -> Bool)
-> (IntVar -> IntVar -> IntVar)
-> (IntVar -> IntVar -> IntVar)
-> Ord IntVar
IntVar -> IntVar -> Bool
IntVar -> IntVar -> Ordering
IntVar -> IntVar -> IntVar
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 :: IntVar -> IntVar -> Ordering
compare :: IntVar -> IntVar -> Ordering
$c< :: IntVar -> IntVar -> Bool
< :: IntVar -> IntVar -> Bool
$c<= :: IntVar -> IntVar -> Bool
<= :: IntVar -> IntVar -> Bool
$c> :: IntVar -> IntVar -> Bool
> :: IntVar -> IntVar -> Bool
$c>= :: IntVar -> IntVar -> Bool
>= :: IntVar -> IntVar -> Bool
$cmax :: IntVar -> IntVar -> IntVar
max :: IntVar -> IntVar -> IntVar
$cmin :: IntVar -> IntVar -> IntVar
min :: IntVar -> IntVar -> IntVar
Ord)

-- | 'UType's are like 'Type's, but also contain unification
--   variables.  'UType' is defined via 'Free', which is also a kind
--   of fixed point (in fact, @Free TypeF@ is the /free monad/ over
--   'TypeF').
--
--   Just as with 'Type', we provide a bunch of pattern synonyms for
--   working with 'UType' as if it were defined directly.
type UType = Free TypeF IntVar

-- | A generic /fold/ for things defined via 'Free' (including, in
--   particular, 'UType').
ucata :: Functor t => (v -> a) -> (t a -> a) -> Free t v -> a
ucata :: forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> Free t v -> a
ucata v -> a
f t a -> a
_ (Pure v
v) = v -> a
f v
v
ucata v -> a
f t a -> a
g (Free t (Free t v)
t) = t a -> a
g ((Free t v -> a) -> t (Free t v) -> t a
forall a b. (a -> b) -> t a -> t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((v -> a) -> (t a -> a) -> Free t v -> a
forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> Free t v -> a
ucata v -> a
f t a -> a
g) t (Free t v)
t)

-- | A quick-and-dirty method for turning an 'IntVar' (used internally
--   as a unification variable) into a unique variable name, by
--   appending a number to the given name.
mkVarName :: Text -> IntVar -> Var
mkVarName :: Text -> IntVar -> Text
mkVarName Text
nm (IntVar Int
v) = Text -> Text -> Text
T.append Text
nm (forall source target. From source target => source -> target
from @String (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
v))

-- | Get all the free unification variables in a 'UType'.
fuvs :: UType -> Set IntVar
fuvs :: UType -> Set IntVar
fuvs = (IntVar -> Set IntVar)
-> (TypeF (Set IntVar) -> Set IntVar) -> UType -> Set IntVar
forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> Free t v -> a
ucata IntVar -> Set IntVar
forall a. a -> Set a
S.singleton TypeF (Set IntVar) -> Set IntVar
forall m. Monoid m => TypeF m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold

-- | For convenience, so we can write /e.g./ @"a"@ instead of @TyVar "a"@.
instance IsString Type where
  fromString :: [Char] -> Type
fromString [Char]
x = Text -> Type
TyVar (forall source target. From source target => source -> target
from @String [Char]
x)

instance IsString UType where
  fromString :: [Char] -> UType
fromString [Char]
x = Text -> UType
UTyVar (forall source target. From source target => source -> target
from @String [Char]
x)

------------------------------------------------------------
-- Generic folding over type representations
------------------------------------------------------------

class Typical t where
  foldT :: (TypeF t -> t) -> t -> t
  rollT :: TypeF t -> t
  fromType :: Type -> t

instance Typical Type where
  foldT :: (TypeF Type -> Type) -> Type -> Type
foldT = (TypeF Type -> Type) -> Type -> Type
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix
  rollT :: TypeF Type -> Type
rollT = TypeF Type -> Type
forall (f :: * -> *). f (Fix f) -> Fix f
Fix
  fromType :: Type -> Type
fromType = Type -> Type
forall a. a -> a
id

instance Typical UType where
  foldT :: (TypeF UType -> UType) -> UType -> UType
foldT = (IntVar -> UType) -> (TypeF UType -> UType) -> UType -> UType
forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> Free t v -> a
ucata IntVar -> UType
forall (f :: * -> *) a. a -> Free f a
Pure
  rollT :: TypeF UType -> UType
rollT = TypeF UType -> UType
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free
  fromType :: Type -> UType
fromType = Type -> UType
Type -> U Type
forall t. WithU t => t -> U t
toU

------------------------------------------------------------
-- Polytypes
------------------------------------------------------------

-- | A @Poly t@ is a universally quantified @t@.  The variables in the
--   list are bound inside the @t@.  For example, the type @forall
--   a. a -> a@ would be represented as @Forall ["a"] (TyFun "a" "a")@.
data Poly t = Forall {forall t. Poly t -> [Text]
ptVars :: [Var], forall t. Poly t -> t
ptBody :: t}
  deriving (Int -> Poly t -> ShowS
[Poly t] -> ShowS
Poly t -> [Char]
(Int -> Poly t -> ShowS)
-> (Poly t -> [Char]) -> ([Poly t] -> ShowS) -> Show (Poly t)
forall t. Show t => Int -> Poly t -> ShowS
forall t. Show t => [Poly t] -> ShowS
forall t. Show t => Poly t -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> Poly t -> ShowS
showsPrec :: Int -> Poly t -> ShowS
$cshow :: forall t. Show t => Poly t -> [Char]
show :: Poly t -> [Char]
$cshowList :: forall t. Show t => [Poly t] -> ShowS
showList :: [Poly t] -> ShowS
Show, Poly t -> Poly t -> Bool
(Poly t -> Poly t -> Bool)
-> (Poly t -> Poly t -> Bool) -> Eq (Poly t)
forall t. Eq t => Poly t -> Poly t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall t. Eq t => Poly t -> Poly t -> Bool
== :: Poly t -> Poly t -> Bool
$c/= :: forall t. Eq t => Poly t -> Poly t -> Bool
/= :: Poly t -> Poly t -> Bool
Eq, (forall a b. (a -> b) -> Poly a -> Poly b)
-> (forall a b. a -> Poly b -> Poly a) -> Functor Poly
forall a b. a -> Poly b -> Poly a
forall a b. (a -> b) -> Poly a -> Poly b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Poly a -> Poly b
fmap :: forall a b. (a -> b) -> Poly a -> Poly b
$c<$ :: forall a b. a -> Poly b -> Poly a
<$ :: forall a b. a -> Poly b -> Poly a
Functor, (forall m. Monoid m => Poly m -> m)
-> (forall m a. Monoid m => (a -> m) -> Poly a -> m)
-> (forall m a. Monoid m => (a -> m) -> Poly a -> m)
-> (forall a b. (a -> b -> b) -> b -> Poly a -> b)
-> (forall a b. (a -> b -> b) -> b -> Poly a -> b)
-> (forall b a. (b -> a -> b) -> b -> Poly a -> b)
-> (forall b a. (b -> a -> b) -> b -> Poly a -> b)
-> (forall a. (a -> a -> a) -> Poly a -> a)
-> (forall a. (a -> a -> a) -> Poly a -> a)
-> (forall a. Poly a -> [a])
-> (forall a. Poly a -> Bool)
-> (forall a. Poly a -> Int)
-> (forall a. Eq a => a -> Poly a -> Bool)
-> (forall a. Ord a => Poly a -> a)
-> (forall a. Ord a => Poly a -> a)
-> (forall a. Num a => Poly a -> a)
-> (forall a. Num a => Poly a -> a)
-> Foldable Poly
forall a. Eq a => a -> Poly a -> Bool
forall a. Num a => Poly a -> a
forall a. Ord a => Poly a -> a
forall m. Monoid m => Poly m -> m
forall a. Poly a -> Bool
forall a. Poly a -> Int
forall a. Poly a -> [a]
forall a. (a -> a -> a) -> Poly a -> a
forall m a. Monoid m => (a -> m) -> Poly a -> m
forall b a. (b -> a -> b) -> b -> Poly a -> b
forall a b. (a -> b -> b) -> b -> Poly a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Poly m -> m
fold :: forall m. Monoid m => Poly m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Poly a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Poly a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Poly a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Poly a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Poly a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Poly a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Poly a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Poly a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Poly a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Poly a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Poly a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Poly a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Poly a -> a
foldr1 :: forall a. (a -> a -> a) -> Poly a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Poly a -> a
foldl1 :: forall a. (a -> a -> a) -> Poly a -> a
$ctoList :: forall a. Poly a -> [a]
toList :: forall a. Poly a -> [a]
$cnull :: forall a. Poly a -> Bool
null :: forall a. Poly a -> Bool
$clength :: forall a. Poly a -> Int
length :: forall a. Poly a -> Int
$celem :: forall a. Eq a => a -> Poly a -> Bool
elem :: forall a. Eq a => a -> Poly a -> Bool
$cmaximum :: forall a. Ord a => Poly a -> a
maximum :: forall a. Ord a => Poly a -> a
$cminimum :: forall a. Ord a => Poly a -> a
minimum :: forall a. Ord a => Poly a -> a
$csum :: forall a. Num a => Poly a -> a
sum :: forall a. Num a => Poly a -> a
$cproduct :: forall a. Num a => Poly a -> a
product :: forall a. Num a => Poly a -> a
Foldable, Functor Poly
Foldable Poly
(Functor Poly, Foldable Poly) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Poly a -> f (Poly b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Poly (f a) -> f (Poly a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Poly a -> m (Poly b))
-> (forall (m :: * -> *) a. Monad m => Poly (m a) -> m (Poly a))
-> Traversable Poly
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Poly (m a) -> m (Poly a)
forall (f :: * -> *) a. Applicative f => Poly (f a) -> f (Poly a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Poly a -> m (Poly b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Poly a -> f (Poly b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Poly a -> f (Poly b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Poly a -> f (Poly b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Poly (f a) -> f (Poly a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Poly (f a) -> f (Poly a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Poly a -> m (Poly b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Poly a -> m (Poly b)
$csequence :: forall (m :: * -> *) a. Monad m => Poly (m a) -> m (Poly a)
sequence :: forall (m :: * -> *) a. Monad m => Poly (m a) -> m (Poly a)
Traversable, Typeable (Poly t)
Typeable (Poly t) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Poly t -> c (Poly t))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Poly t))
-> (Poly t -> Constr)
-> (Poly t -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Poly t)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Poly t)))
-> ((forall b. Data b => b -> b) -> Poly t -> Poly t)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Poly t -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Poly t -> r)
-> (forall u. (forall d. Data d => d -> u) -> Poly t -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Poly t -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Poly t -> m (Poly t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Poly t -> m (Poly t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Poly t -> m (Poly t))
-> Data (Poly t)
Poly t -> Constr
Poly t -> DataType
(forall b. Data b => b -> b) -> Poly t -> Poly t
forall t. Data t => Typeable (Poly t)
forall t. Data t => Poly t -> Constr
forall t. Data t => Poly t -> DataType
forall t.
Data t =>
(forall b. Data b => b -> b) -> Poly t -> Poly t
forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> Poly t -> u
forall t u. Data t => (forall d. Data d => d -> u) -> Poly t -> [u]
forall t r r'.
Data t =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
forall t r r'.
Data t =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Poly t)
forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Poly t -> c (Poly t)
forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Poly t))
forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Poly t))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Poly t -> u
forall u. (forall d. Data d => d -> u) -> Poly t -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Poly t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Poly t -> c (Poly t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Poly t))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Poly t))
$cgfoldl :: forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Poly t -> c (Poly t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Poly t -> c (Poly t)
$cgunfold :: forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Poly t)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Poly t)
$ctoConstr :: forall t. Data t => Poly t -> Constr
toConstr :: Poly t -> Constr
$cdataTypeOf :: forall t. Data t => Poly t -> DataType
dataTypeOf :: Poly t -> DataType
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Poly t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Poly t))
$cdataCast2 :: forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Poly t))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Poly t))
$cgmapT :: forall t.
Data t =>
(forall b. Data b => b -> b) -> Poly t -> Poly t
gmapT :: (forall b. Data b => b -> b) -> Poly t -> Poly t
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
$cgmapQr :: forall t r r'.
Data t =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
$cgmapQ :: forall t u. Data t => (forall d. Data d => d -> u) -> Poly t -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Poly t -> [u]
$cgmapQi :: forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> Poly t -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Poly t -> u
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
$cgmapMp :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
$cgmapMo :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
Data, (forall x. Poly t -> Rep (Poly t) x)
-> (forall x. Rep (Poly t) x -> Poly t) -> Generic (Poly t)
forall x. Rep (Poly t) x -> Poly t
forall x. Poly t -> Rep (Poly t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (Poly t) x -> Poly t
forall t x. Poly t -> Rep (Poly t) x
$cfrom :: forall t x. Poly t -> Rep (Poly t) x
from :: forall x. Poly t -> Rep (Poly t) x
$cto :: forall t x. Rep (Poly t) x -> Poly t
to :: forall x. Rep (Poly t) x -> Poly t
Generic, Maybe (Poly t)
Value -> Parser [Poly t]
Value -> Parser (Poly t)
(Value -> Parser (Poly t))
-> (Value -> Parser [Poly t])
-> Maybe (Poly t)
-> FromJSON (Poly t)
forall t. FromJSON t => Maybe (Poly t)
forall t. FromJSON t => Value -> Parser [Poly t]
forall t. FromJSON t => Value -> Parser (Poly t)
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: forall t. FromJSON t => Value -> Parser (Poly t)
parseJSON :: Value -> Parser (Poly t)
$cparseJSONList :: forall t. FromJSON t => Value -> Parser [Poly t]
parseJSONList :: Value -> Parser [Poly t]
$comittedField :: forall t. FromJSON t => Maybe (Poly t)
omittedField :: Maybe (Poly t)
FromJSON, [Poly t] -> Value
[Poly t] -> Encoding
Poly t -> Bool
Poly t -> Value
Poly t -> Encoding
(Poly t -> Value)
-> (Poly t -> Encoding)
-> ([Poly t] -> Value)
-> ([Poly t] -> Encoding)
-> (Poly t -> Bool)
-> ToJSON (Poly t)
forall t. ToJSON t => [Poly t] -> Value
forall t. ToJSON t => [Poly t] -> Encoding
forall t. ToJSON t => Poly t -> Bool
forall t. ToJSON t => Poly t -> Value
forall t. ToJSON t => Poly t -> Encoding
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: forall t. ToJSON t => Poly t -> Value
toJSON :: Poly t -> Value
$ctoEncoding :: forall t. ToJSON t => Poly t -> Encoding
toEncoding :: Poly t -> Encoding
$ctoJSONList :: forall t. ToJSON t => [Poly t] -> Value
toJSONList :: [Poly t] -> Value
$ctoEncodingList :: forall t. ToJSON t => [Poly t] -> Encoding
toEncodingList :: [Poly t] -> Encoding
$comitField :: forall t. ToJSON t => Poly t -> Bool
omitField :: Poly t -> Bool
ToJSON)

-- | A polytype without unification variables.
type Polytype = Poly Type

-- | A polytype with unification variables.
type UPolytype = Poly UType

------------------------------------------------------------
-- WithU
------------------------------------------------------------

-- | In several cases we have two versions of something: a "normal"
--   version, and a @U@ version with unification variables in it
--   (/e.g./ 'Type' vs 'UType', 'Polytype' vs 'UPolytype', 'TCtx' vs
--   'UCtx'). This class abstracts over the process of converting back
--   and forth between them.
--
--   In particular, @'WithU' t@ represents the fact that the type @t@
--   also has a @U@ counterpart, with a way to convert back and forth.
--   Note, however, that converting back may be "unsafe" in the sense
--   that it requires an extra burden of proof to guarantee that it is
--   used only on inputs that are safe.
class WithU t where
  -- | The associated "@U@-version" of the type @t@.
  type U t :: Data.Kind.Type

  -- | Convert from @t@ to its associated "@U@-version".  This
  --   direction is always safe (we simply have no unification
  --   variables even though the type allows it).
  toU :: t -> U t

  -- | Convert from the associated "@U@-version" back to @t@.
  --   Generally, this direction requires somehow knowing that there
  --   are no longer any unification variables in the value being
  --   converted.
  fromU :: U t -> Maybe t

-- | 'Type' is an instance of 'WithU', with associated type 'UType'.
instance WithU Type where
  type U Type = UType
  toU :: Type -> U Type
toU = (TypeF UType -> UType) -> Type -> UType
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix TypeF UType -> UType
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free
  fromU :: U Type -> Maybe Type
fromU = (IntVar -> Maybe Type)
-> (TypeF (Maybe Type) -> Maybe Type) -> UType -> Maybe Type
forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> Free t v -> a
ucata (Maybe Type -> IntVar -> Maybe Type
forall a b. a -> b -> a
const Maybe Type
forall a. Maybe a
Nothing) ((TypeF Type -> Type) -> Maybe (TypeF Type) -> Maybe Type
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeF Type -> Type
forall (f :: * -> *). f (Fix f) -> Fix f
wrapFix (Maybe (TypeF Type) -> Maybe Type)
-> (TypeF (Maybe Type) -> Maybe (TypeF Type))
-> TypeF (Maybe Type)
-> Maybe Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeF (Maybe Type) -> Maybe (TypeF Type)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
sequence)

-- | A 'WithU' instance can be lifted through any functor (including,
--   in particular, 'Ctx' and 'Poly').
instance (WithU t, Traversable f) => WithU (f t) where
  type U (f t) = f (U t)
  toU :: f t -> U (f t)
toU = (t -> U t) -> f t -> f (U t)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t -> U t
forall t. WithU t => t -> U t
toU
  fromU :: U (f t) -> Maybe (f t)
fromU = (U t -> Maybe t) -> f (U t) -> Maybe (f t)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse U t -> Maybe t
forall t. WithU t => U t -> Maybe t
fromU

------------------------------------------------------------
-- Pattern synonyms
------------------------------------------------------------

--------------------------------------------------
-- Type

pattern TyConApp :: TyCon -> [Type] -> Type
pattern $mTyConApp :: forall {r}. Type -> (TyCon -> [Type] -> r) -> ((# #) -> r) -> r
$bTyConApp :: TyCon -> [Type] -> Type
TyConApp c tys = Fix (TyConF c tys)

pattern TyBase :: BaseTy -> Type
pattern $mTyBase :: forall {r}. Type -> (BaseTy -> r) -> ((# #) -> r) -> r
$bTyBase :: BaseTy -> Type
TyBase b = TyConApp (TCBase b) []

pattern TyVar :: Var -> Type
pattern $mTyVar :: forall {r}. Type -> (Text -> r) -> ((# #) -> r) -> r
$bTyVar :: Text -> Type
TyVar v = Fix (TyVarF v)

pattern TyVoid :: Type
pattern $mTyVoid :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
$bTyVoid :: Type
TyVoid = TyBase BVoid

pattern TyUnit :: Type
pattern $mTyUnit :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
$bTyUnit :: Type
TyUnit = TyBase BUnit

pattern TyInt :: Type
pattern $mTyInt :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
$bTyInt :: Type
TyInt = TyBase BInt

pattern TyText :: Type
pattern $mTyText :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
$bTyText :: Type
TyText = TyBase BText

pattern TyDir :: Type
pattern $mTyDir :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
$bTyDir :: Type
TyDir = TyBase BDir

pattern TyBool :: Type
pattern $mTyBool :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
$bTyBool :: Type
TyBool = TyBase BBool

pattern TyActor :: Type
pattern $mTyActor :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
$bTyActor :: Type
TyActor = TyBase BActor

pattern TyKey :: Type
pattern $mTyKey :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
$bTyKey :: Type
TyKey = TyBase BKey

infixr 5 :+:

pattern (:+:) :: Type -> Type -> Type
pattern ty1 $m:+: :: forall {r}. Type -> (Type -> Type -> r) -> ((# #) -> r) -> r
$b:+: :: Type -> Type -> Type
:+: ty2 = TyConApp TCSum [ty1, ty2]

infixr 6 :*:

pattern (:*:) :: Type -> Type -> Type
pattern ty1 $m:*: :: forall {r}. Type -> (Type -> Type -> r) -> ((# #) -> r) -> r
$b:*: :: Type -> Type -> Type
:*: ty2 = TyConApp TCProd [ty1, ty2]

infixr 1 :->:

pattern (:->:) :: Type -> Type -> Type
pattern ty1 $m:->: :: forall {r}. Type -> (Type -> Type -> r) -> ((# #) -> r) -> r
$b:->: :: Type -> Type -> Type
:->: ty2 = TyConApp TCFun [ty1, ty2]

pattern TyRcd :: Map Var Type -> Type
pattern $mTyRcd :: forall {r}. Type -> (Map Text Type -> r) -> ((# #) -> r) -> r
$bTyRcd :: Map Text Type -> Type
TyRcd m = Fix (TyRcdF m)

pattern TyCmd :: Type -> Type
pattern $mTyCmd :: forall {r}. Type -> (Type -> r) -> ((# #) -> r) -> r
$bTyCmd :: Type -> Type
TyCmd ty = TyConApp TCCmd [ty]

pattern TyDelay :: Type -> Type
pattern $mTyDelay :: forall {r}. Type -> (Type -> r) -> ((# #) -> r) -> r
$bTyDelay :: Type -> Type
TyDelay ty = TyConApp TCDelay [ty]

pattern TyUser :: Var -> [Type] -> Type
pattern $mTyUser :: forall {r}. Type -> (Text -> [Type] -> r) -> ((# #) -> r) -> r
$bTyUser :: Text -> [Type] -> Type
TyUser v tys = TyConApp (TCUser v) tys

pattern TyRec :: Var -> Type -> Type
pattern $mTyRec :: forall {r}. Type -> (Text -> Type -> r) -> ((# #) -> r) -> r
$bTyRec :: Text -> Type -> Type
TyRec x ty = Fix (TyRecF x ty)

--------------------------------------------------
-- UType

pattern UTyConApp :: TyCon -> [UType] -> UType
pattern $mUTyConApp :: forall {r}. UType -> (TyCon -> [UType] -> r) -> ((# #) -> r) -> r
$bUTyConApp :: TyCon -> [UType] -> UType
UTyConApp c tys = Free (TyConF c tys)

pattern UTyBase :: BaseTy -> UType
pattern $mUTyBase :: forall {r}. UType -> (BaseTy -> r) -> ((# #) -> r) -> r
$bUTyBase :: BaseTy -> UType
UTyBase b = UTyConApp (TCBase b) []

pattern UTyVar :: Var -> UType
pattern $mUTyVar :: forall {r}. UType -> (Text -> r) -> ((# #) -> r) -> r
$bUTyVar :: Text -> UType
UTyVar v = Free (TyVarF v)

pattern UTyVoid :: UType
pattern $mUTyVoid :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
$bUTyVoid :: UType
UTyVoid = UTyBase BVoid

pattern UTyUnit :: UType
pattern $mUTyUnit :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
$bUTyUnit :: UType
UTyUnit = UTyBase BUnit

pattern UTyInt :: UType
pattern $mUTyInt :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
$bUTyInt :: UType
UTyInt = UTyBase BInt

pattern UTyText :: UType
pattern $mUTyText :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
$bUTyText :: UType
UTyText = UTyBase BText

pattern UTyDir :: UType
pattern $mUTyDir :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
$bUTyDir :: UType
UTyDir = UTyBase BDir

pattern UTyBool :: UType
pattern $mUTyBool :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
$bUTyBool :: UType
UTyBool = UTyBase BBool

pattern UTyActor :: UType
pattern $mUTyActor :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
$bUTyActor :: UType
UTyActor = UTyBase BActor

pattern UTyKey :: UType
pattern $mUTyKey :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
$bUTyKey :: UType
UTyKey = UTyBase BKey

pattern UTySum :: UType -> UType -> UType
pattern $mUTySum :: forall {r}. UType -> (UType -> UType -> r) -> ((# #) -> r) -> r
$bUTySum :: UType -> UType -> UType
UTySum ty1 ty2 = UTyConApp TCSum [ty1, ty2]

pattern UTyProd :: UType -> UType -> UType
pattern $mUTyProd :: forall {r}. UType -> (UType -> UType -> r) -> ((# #) -> r) -> r
$bUTyProd :: UType -> UType -> UType
UTyProd ty1 ty2 = UTyConApp TCProd [ty1, ty2]

pattern UTyFun :: UType -> UType -> UType
pattern $mUTyFun :: forall {r}. UType -> (UType -> UType -> r) -> ((# #) -> r) -> r
$bUTyFun :: UType -> UType -> UType
UTyFun ty1 ty2 = UTyConApp TCFun [ty1, ty2]

pattern UTyRcd :: Map Var UType -> UType
pattern $mUTyRcd :: forall {r}. UType -> (Map Text UType -> r) -> ((# #) -> r) -> r
$bUTyRcd :: Map Text UType -> UType
UTyRcd m = Free (TyRcdF m)

pattern UTyCmd :: UType -> UType
pattern $mUTyCmd :: forall {r}. UType -> (UType -> r) -> ((# #) -> r) -> r
$bUTyCmd :: UType -> UType
UTyCmd ty = UTyConApp TCCmd [ty]

pattern UTyDelay :: UType -> UType
pattern $mUTyDelay :: forall {r}. UType -> (UType -> r) -> ((# #) -> r) -> r
$bUTyDelay :: UType -> UType
UTyDelay ty = UTyConApp TCDelay [ty]

pattern UTyUser :: Var -> [UType] -> UType
pattern $mUTyUser :: forall {r}. UType -> (Text -> [UType] -> r) -> ((# #) -> r) -> r
$bUTyUser :: Text -> [UType] -> UType
UTyUser v tys = UTyConApp (TCUser v) tys

pattern UTyRec :: Var -> UType -> UType
pattern $mUTyRec :: forall {r}. UType -> (Text -> UType -> r) -> ((# #) -> r) -> r
$bUTyRec :: Text -> UType -> UType
UTyRec x ty = Free (TyRecF x ty)

pattern PolyUnit :: Polytype
pattern $mPolyUnit :: forall {r}. Polytype -> ((# #) -> r) -> ((# #) -> r) -> r
$bPolyUnit :: Polytype
PolyUnit = Forall [] (TyCmd TyUnit)

------------------------------------------------------------
-- Contexts
------------------------------------------------------------

-- | A @TCtx@ is a mapping from variables to polytypes.  We generally
--   get one of these at the end of the type inference process.
type TCtx = Ctx Polytype

-- | A @UCtx@ is a mapping from variables to polytypes with
--   unification variables.  We generally have one of these while we
--   are in the midst of the type inference process.
type UCtx = Ctx UPolytype

------------------------------------------------------------
-- Type definitions
------------------------------------------------------------

data TydefInfo = TydefInfo
  { TydefInfo -> Polytype
_tydefType :: Polytype
  , TydefInfo -> Arity
_tydefArity :: Arity
  }
  deriving (TydefInfo -> TydefInfo -> Bool
(TydefInfo -> TydefInfo -> Bool)
-> (TydefInfo -> TydefInfo -> Bool) -> Eq TydefInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TydefInfo -> TydefInfo -> Bool
== :: TydefInfo -> TydefInfo -> Bool
$c/= :: TydefInfo -> TydefInfo -> Bool
/= :: TydefInfo -> TydefInfo -> Bool
Eq, Int -> TydefInfo -> ShowS
[TydefInfo] -> ShowS
TydefInfo -> [Char]
(Int -> TydefInfo -> ShowS)
-> (TydefInfo -> [Char])
-> ([TydefInfo] -> ShowS)
-> Show TydefInfo
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TydefInfo -> ShowS
showsPrec :: Int -> TydefInfo -> ShowS
$cshow :: TydefInfo -> [Char]
show :: TydefInfo -> [Char]
$cshowList :: [TydefInfo] -> ShowS
showList :: [TydefInfo] -> ShowS
Show, (forall x. TydefInfo -> Rep TydefInfo x)
-> (forall x. Rep TydefInfo x -> TydefInfo) -> Generic TydefInfo
forall x. Rep TydefInfo x -> TydefInfo
forall x. TydefInfo -> Rep TydefInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TydefInfo -> Rep TydefInfo x
from :: forall x. TydefInfo -> Rep TydefInfo x
$cto :: forall x. Rep TydefInfo x -> TydefInfo
to :: forall x. Rep TydefInfo x -> TydefInfo
Generic, Typeable TydefInfo
Typeable TydefInfo =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TydefInfo -> c TydefInfo)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TydefInfo)
-> (TydefInfo -> Constr)
-> (TydefInfo -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TydefInfo))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TydefInfo))
-> ((forall b. Data b => b -> b) -> TydefInfo -> TydefInfo)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TydefInfo -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TydefInfo -> r)
-> (forall u. (forall d. Data d => d -> u) -> TydefInfo -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> TydefInfo -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TydefInfo -> m TydefInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TydefInfo -> m TydefInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TydefInfo -> m TydefInfo)
-> Data TydefInfo
TydefInfo -> Constr
TydefInfo -> DataType
(forall b. Data b => b -> b) -> TydefInfo -> TydefInfo
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TydefInfo -> u
forall u. (forall d. Data d => d -> u) -> TydefInfo -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TydefInfo -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TydefInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TydefInfo -> m TydefInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TydefInfo -> m TydefInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TydefInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TydefInfo -> c TydefInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TydefInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TydefInfo)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TydefInfo -> c TydefInfo
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TydefInfo -> c TydefInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TydefInfo
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TydefInfo
$ctoConstr :: TydefInfo -> Constr
toConstr :: TydefInfo -> Constr
$cdataTypeOf :: TydefInfo -> DataType
dataTypeOf :: TydefInfo -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TydefInfo)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TydefInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TydefInfo)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TydefInfo)
$cgmapT :: (forall b. Data b => b -> b) -> TydefInfo -> TydefInfo
gmapT :: (forall b. Data b => b -> b) -> TydefInfo -> TydefInfo
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TydefInfo -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TydefInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TydefInfo -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TydefInfo -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TydefInfo -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> TydefInfo -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TydefInfo -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TydefInfo -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TydefInfo -> m TydefInfo
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TydefInfo -> m TydefInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TydefInfo -> m TydefInfo
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TydefInfo -> m TydefInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TydefInfo -> m TydefInfo
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TydefInfo -> m TydefInfo
Data, Maybe TydefInfo
Value -> Parser [TydefInfo]
Value -> Parser TydefInfo
(Value -> Parser TydefInfo)
-> (Value -> Parser [TydefInfo])
-> Maybe TydefInfo
-> FromJSON TydefInfo
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser TydefInfo
parseJSON :: Value -> Parser TydefInfo
$cparseJSONList :: Value -> Parser [TydefInfo]
parseJSONList :: Value -> Parser [TydefInfo]
$comittedField :: Maybe TydefInfo
omittedField :: Maybe TydefInfo
FromJSON, [TydefInfo] -> Value
[TydefInfo] -> Encoding
TydefInfo -> Bool
TydefInfo -> Value
TydefInfo -> Encoding
(TydefInfo -> Value)
-> (TydefInfo -> Encoding)
-> ([TydefInfo] -> Value)
-> ([TydefInfo] -> Encoding)
-> (TydefInfo -> Bool)
-> ToJSON TydefInfo
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: TydefInfo -> Value
toJSON :: TydefInfo -> Value
$ctoEncoding :: TydefInfo -> Encoding
toEncoding :: TydefInfo -> Encoding
$ctoJSONList :: [TydefInfo] -> Value
toJSONList :: [TydefInfo] -> Value
$ctoEncodingList :: [TydefInfo] -> Encoding
toEncodingList :: [TydefInfo] -> Encoding
$comitField :: TydefInfo -> Bool
omitField :: TydefInfo -> Bool
ToJSON)

makeLenses ''TydefInfo

-- | A @TDCtx@ is a mapping from user-defined type constructor names
--   to their definitions and arities/kinds.
type TDCtx = Ctx TydefInfo

-- | Expand an application "T ty1 ty2 ... tyn" by looking up the
--   definition of T and substituting ty1 .. tyn for its arguments.
--
--   Note that this has already been kind-checked so we know the
--   number of arguments must match up; we don't worry about what
--   happens if the lists have different lengths since in theory that
--   can never happen.
expandTydef :: (Has (Reader TDCtx) sig m, Typical t) => Var -> [t] -> m t
expandTydef :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) t.
(Has (Reader TDCtx) sig m, Typical t) =>
Text -> [t] -> m t
expandTydef Text
userTyCon [t]
tys = do
  Maybe TydefInfo
mtydefInfo <- Text -> m (Maybe TydefInfo)
forall t (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader (Ctx t)) sig m =>
Text -> m (Maybe t)
Ctx.lookupR Text
userTyCon
  TDCtx
tdCtx <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @TDCtx
  -- In theory, if everything has kind checked, we should never encounter an undefined
  -- type constructor here.
  let errMsg :: [Char]
errMsg =
        forall target source. From source target => source -> target
into @String (Text -> [Char]) -> Text -> [Char]
forall a b. (a -> b) -> a -> b
$
          [Text] -> Text
T.unwords
            [ Text
"Encountered undefined type constructor"
            , Text
userTyCon
            , Text
"in expandTyDef"
            , Text -> Text
parens (Text
"tdCtx = " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> TDCtx -> Text
forall a. Show a => a -> Text
showT TDCtx
tdCtx)
            ]
      tydefInfo :: TydefInfo
tydefInfo = TydefInfo -> Maybe TydefInfo -> TydefInfo
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> TydefInfo
forall a. HasCallStack => [Char] -> a
error [Char]
errMsg) Maybe TydefInfo
mtydefInfo
  t -> m t
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (t -> m t) -> t -> m t
forall a b. (a -> b) -> a -> b
$ TydefInfo -> [t] -> t
forall t. Typical t => TydefInfo -> [t] -> t
substTydef TydefInfo
tydefInfo [t]
tys

-- | Given the definition of a type alias, substitute the given
--   arguments into its body and return the resulting type.
substTydef :: forall t. Typical t => TydefInfo -> [t] -> t
substTydef :: forall t. Typical t => TydefInfo -> [t] -> t
substTydef (TydefInfo (Forall [Text]
as Type
ty) Arity
_) [t]
tys = forall t. Typical t => (TypeF t -> t) -> t -> t
foldT @t TypeF t -> t
substF (Type -> t
forall t. Typical t => Type -> t
fromType Type
ty)
 where
  argMap :: Map Text t
argMap = [(Text, t)] -> Map Text t
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Text, t)] -> Map Text t) -> [(Text, t)] -> Map Text t
forall a b. (a -> b) -> a -> b
$ [Text] -> [t] -> [(Text, t)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
as [t]
tys

  substF :: TypeF t -> t
substF tyF :: TypeF t
tyF@(TyVarF Text
x) = case Text -> Map Text t -> Maybe t
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
x Map Text t
argMap of
    Maybe t
Nothing -> TypeF t -> t
forall t. Typical t => TypeF t -> t
rollT TypeF t
tyF
    Just t
ty' -> t
ty'
  substF TypeF t
tyF = TypeF t -> t
forall t. Typical t => TypeF t -> t
rollT TypeF t
tyF

-- | Replace a type alias with its definition everywhere it occurs
--   inside a type.  Typically this is done when reporting the type of
--   a term containing a local tydef: since the tydef is local we
--   can't use it in the reported type.
elimTydef :: forall t. Typical t => Var -> TydefInfo -> t -> t
elimTydef :: forall t. Typical t => Text -> TydefInfo -> t -> t
elimTydef Text
x TydefInfo
tdInfo = (TypeF t -> t) -> t -> t
forall t. Typical t => (TypeF t -> t) -> t -> t
foldT TypeF t -> t
substF
 where
  substF :: TypeF t -> t
substF = \case
    TyConF (TCUser Text
u) [t]
tys | Text
u Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
x -> TydefInfo -> [t] -> t
forall t. Typical t => TydefInfo -> [t] -> t
substTydef TydefInfo
tdInfo [t]
tys
    TypeF t
tyF -> TypeF t -> t
forall t. Typical t => TypeF t -> t
rollT TypeF t
tyF

------------------------------------------------------------
-- Arity
------------------------------------------------------------

-- | The arity, /i.e./ number of type arguments, of each type
--   constructor.  Eventually, if we generalize to higher-kinded
--   types, we'll need to upgrade this to return a full-fledged kind
--   instead of just an arity.
tcArity :: TDCtx -> TyCon -> Maybe Arity
tcArity :: TDCtx -> TyCon -> Maybe Arity
tcArity TDCtx
tydefs =
  (Int -> Arity) -> Maybe Int -> Maybe Arity
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Arity
Arity (Maybe Int -> Maybe Arity)
-> (TyCon -> Maybe Int) -> TyCon -> Maybe Arity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    TCBase BaseTy
_ -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0
    TyCon
TCCmd -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
    TyCon
TCDelay -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
    TyCon
TCSum -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
2
    TyCon
TCProd -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
2
    TyCon
TCFun -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
2
    TCUser Text
t -> Arity -> Int
getArity (Arity -> Int) -> (TydefInfo -> Arity) -> TydefInfo -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Arity TydefInfo Arity -> TydefInfo -> Arity
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Arity TydefInfo Arity
Lens' TydefInfo Arity
tydefArity (TydefInfo -> Int) -> Maybe TydefInfo -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> TDCtx -> Maybe TydefInfo
forall t. Text -> Ctx t -> Maybe t
Ctx.lookup Text
t TDCtx
tydefs

------------------------------------------------------------
-- Recursive type utilities
------------------------------------------------------------

-- | @unfoldRec x t@ unfolds the recursive type @rec x. t@ one step,
--   to @t [(rec x. t) / x]@.
unfoldRec :: SubstRec t => Var -> t -> t
unfoldRec :: forall t. SubstRec t => Text -> t -> t
unfoldRec Text
x t
ty = TypeF t -> t -> Nat -> t
forall t. SubstRec t => TypeF t -> t -> Nat -> t
substRec (Text -> t -> TypeF t
forall t. Text -> t -> TypeF t
TyRecF Text
x t
ty) t
ty Nat
NZ

-- | Class of type-like things where we can substitute for a bound de
--   Bruijn variable.
class SubstRec t where
  -- | @substRec s t n@ substitutes @s@ for the bound de Bruijn variable
  --   @n@ everywhere in @t@.
  substRec :: TypeF t -> t -> Nat -> t

instance SubstRec (Free TypeF v) where
  substRec :: TypeF (Free TypeF v) -> Free TypeF v -> Nat -> Free TypeF v
substRec TypeF (Free TypeF v)
s = (v -> Nat -> Free TypeF v)
-> (TypeF (Nat -> Free TypeF v) -> Nat -> Free TypeF v)
-> Free TypeF v
-> Nat
-> Free TypeF v
forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> Free t v -> a
ucata (\v
i Nat
_ -> v -> Free TypeF v
forall (f :: * -> *) a. a -> Free f a
Pure v
i) ((TypeF (Nat -> Free TypeF v) -> Nat -> Free TypeF v)
 -> Free TypeF v -> Nat -> Free TypeF v)
-> (TypeF (Nat -> Free TypeF v) -> Nat -> Free TypeF v)
-> Free TypeF v
-> Nat
-> Free TypeF v
forall a b. (a -> b) -> a -> b
$ \TypeF (Nat -> Free TypeF v)
f Nat
i -> case TypeF (Nat -> Free TypeF v)
f of
    TyRecVarF Nat
j
      | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
j -> TypeF (Free TypeF v) -> Free TypeF v
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free TypeF (Free TypeF v)
s
      | Bool
otherwise -> TypeF (Free TypeF v) -> Free TypeF v
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free (Nat -> TypeF (Free TypeF v)
forall t. Nat -> TypeF t
TyRecVarF Nat
j)
    TyRecF Text
x Nat -> Free TypeF v
g -> TypeF (Free TypeF v) -> Free TypeF v
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free (Text -> Free TypeF v -> TypeF (Free TypeF v)
forall t. Text -> t -> TypeF t
TyRecF Text
x (Nat -> Free TypeF v
g (Nat -> Nat
NS Nat
i)))
    TypeF (Nat -> Free TypeF v)
_ -> TypeF (Free TypeF v) -> Free TypeF v
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free (((Nat -> Free TypeF v) -> Free TypeF v)
-> TypeF (Nat -> Free TypeF v) -> TypeF (Free TypeF v)
forall a b. (a -> b) -> TypeF a -> TypeF b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Nat -> Free TypeF v) -> Nat -> Free TypeF v
forall a b. (a -> b) -> a -> b
$ Nat
i) TypeF (Nat -> Free TypeF v)
f)

instance SubstRec Type where
  substRec :: TypeF Type -> Type -> Nat -> Type
substRec TypeF Type
s = (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) -> Type -> Nat -> Type)
-> (TypeF (Nat -> Type) -> Nat -> Type) -> Type -> Nat -> Type
forall a b. (a -> b) -> a -> b
$ \TypeF (Nat -> Type)
f Nat
i -> case TypeF (Nat -> Type)
f of
    TyRecVarF Nat
j
      | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
j -> TypeF Type -> Type
forall (f :: * -> *). f (Fix f) -> Fix f
Fix TypeF Type
s
      | Bool
otherwise -> TypeF Type -> Type
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Nat -> TypeF Type
forall t. Nat -> TypeF t
TyRecVarF Nat
j)
    TyRecF Text
x Nat -> Type
g -> TypeF Type -> Type
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Text -> Type -> TypeF Type
forall t. Text -> t -> TypeF t
TyRecF Text
x (Nat -> Type
g (Nat -> Nat
NS Nat
i)))
    TypeF (Nat -> Type)
_ -> 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)
f)

------------------------------------------------------------
-- Reducing types to WHNF
------------------------------------------------------------

-- | Reduce a type to weak head normal form, i.e. keep unfold type
--   aliases and recursive types just until the top-level constructor
--   of the type is neither @rec@ nor an application of a type alias.
whnfType :: TDCtx -> Type -> Type
whnfType :: TDCtx -> Type -> Type
whnfType TDCtx
tdCtx = Identity Type -> Type
forall a. Identity a -> a
run (Identity Type -> Type) -> (Type -> Identity Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TDCtx -> ReaderC TDCtx Identity Type -> Identity Type
forall r (m :: * -> *) a. r -> ReaderC r m a -> m a
runReader TDCtx
tdCtx (ReaderC TDCtx Identity Type -> Identity Type)
-> (Type -> ReaderC TDCtx Identity Type) -> Type -> Identity Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ReaderC TDCtx Identity Type
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader TDCtx) sig m =>
Type -> m Type
go
 where
  go :: Has (Reader TDCtx) sig m => Type -> m Type
  go :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader TDCtx) sig m =>
Type -> m Type
go = \case
    TyUser Text
u [Type]
tys -> Text -> [Type] -> m Type
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) t.
(Has (Reader TDCtx) sig m, Typical t) =>
Text -> [t] -> m t
expandTydef Text
u [Type]
tys m Type -> (Type -> m Type) -> m Type
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> m Type
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader TDCtx) sig m =>
Type -> m Type
go
    TyRec Text
x Type
ty -> Type -> m Type
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader TDCtx) sig m =>
Type -> m Type
go (Text -> Type -> Type
forall t. SubstRec t => Text -> t -> t
unfoldRec Text
x Type
ty)
    Type
ty -> Type -> m Type
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty