{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

-- for the Data IntVar instance

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

  -- * @Type@
  Type,
  tyVars,
  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,

  -- * @UType@
  UType,
  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,

  -- ** Utilities
  ucata,
  mkVarName,

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

  -- * Contexts
  TCtx,
  UCtx,

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

import Control.Monad (guard)
import Control.Unification
import Control.Unification.IntVar
import Data.Aeson (FromJSON, ToJSON)
import Data.Data (Data)
import Data.Foldable (fold)
import Data.Function (on)
import Data.Functor.Fixedpoint
import Data.Kind qualified
import Data.Map.Merge.Strict qualified as M
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as M
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
import Witch

------------------------------------------------------------
-- 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BaseTy -> BaseTy -> Bool
$c/= :: BaseTy -> BaseTy -> Bool
== :: BaseTy -> BaseTy -> Bool
$c== :: BaseTy -> BaseTy -> Bool
Eq, Eq 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
min :: BaseTy -> BaseTy -> BaseTy
$cmin :: BaseTy -> BaseTy -> BaseTy
max :: BaseTy -> BaseTy -> BaseTy
$cmax :: BaseTy -> BaseTy -> BaseTy
>= :: BaseTy -> BaseTy -> Bool
$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
compare :: BaseTy -> BaseTy -> Ordering
$ccompare :: BaseTy -> BaseTy -> Ordering
Ord, Int -> BaseTy -> ShowS
[BaseTy] -> ShowS
BaseTy -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BaseTy] -> ShowS
$cshowList :: [BaseTy] -> ShowS
show :: BaseTy -> String
$cshow :: BaseTy -> String
showsPrec :: Int -> BaseTy -> ShowS
$cshowsPrec :: Int -> BaseTy -> ShowS
Show, Typeable BaseTy
BaseTy -> DataType
BaseTy -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
gmapT :: (forall b. Data b => b -> b) -> BaseTy -> BaseTy
$cgmapT :: (forall b. Data b => b -> b) -> BaseTy -> BaseTy
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
dataTypeOf :: BaseTy -> DataType
$cdataTypeOf :: BaseTy -> DataType
toConstr :: BaseTy -> Constr
$ctoConstr :: BaseTy -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
Data, 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
$cto :: forall x. Rep BaseTy x -> BaseTy
$cfrom :: forall x. BaseTy -> Rep BaseTy x
Generic, Value -> Parser [BaseTy]
Value -> Parser BaseTy
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [BaseTy]
$cparseJSONList :: Value -> Parser [BaseTy]
parseJSON :: Value -> Parser BaseTy
$cparseJSON :: Value -> Parser BaseTy
FromJSON, [BaseTy] -> Encoding
[BaseTy] -> Value
BaseTy -> Encoding
BaseTy -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [BaseTy] -> Encoding
$ctoEncodingList :: [BaseTy] -> Encoding
toJSONList :: [BaseTy] -> Value
$ctoJSONList :: [BaseTy] -> Value
toEncoding :: BaseTy -> Encoding
$ctoEncoding :: BaseTy -> Encoding
toJSON :: BaseTy -> Value
$ctoJSON :: BaseTy -> Value
ToJSON)

-- | 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 work with the @unification-fd@ package (see
--   https://byorgey.wordpress.com/2021/09/08/implementing-hindley-milner-with-the-unification-fd-library/).
data TypeF t
  = -- | A base type.
    TyBaseF BaseTy
  | -- | A type variable.
    TyVarF Var
  | -- | Commands, with return type.  Note that
    --   commands form a monad.
    TyCmdF t
  | -- | Type of delayed computations.
    TyDelayF t
  | -- | Sum type.
    TySumF t t
  | -- | Product type.
    TyProdF t t
  | -- | Function type.
    TyFunF t t
  | -- | Record type.
    TyRcdF (Map Var t)
  deriving (Int -> TypeF t -> ShowS
forall t. Show t => Int -> TypeF t -> ShowS
forall t. Show t => [TypeF t] -> ShowS
forall t. Show t => TypeF t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeF t] -> ShowS
$cshowList :: forall t. Show t => [TypeF t] -> ShowS
show :: TypeF t -> String
$cshow :: forall t. Show t => TypeF t -> String
showsPrec :: Int -> TypeF t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> TypeF t -> ShowS
Show, TypeF t -> TypeF t -> Bool
forall t. Eq t => TypeF t -> TypeF t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeF t -> TypeF t -> Bool
$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
Eq, 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
<$ :: forall a b. a -> TypeF b -> TypeF a
$c<$ :: forall a b. a -> TypeF b -> TypeF a
fmap :: forall a b. (a -> b) -> TypeF a -> TypeF b
$cfmap :: forall a b. (a -> b) -> TypeF a -> TypeF b
Functor, 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
product :: forall a. Num a => TypeF a -> a
$cproduct :: forall a. Num a => TypeF a -> a
sum :: forall a. Num a => TypeF a -> a
$csum :: forall a. Num a => TypeF a -> a
minimum :: forall a. Ord a => TypeF a -> a
$cminimum :: forall a. Ord a => TypeF a -> a
maximum :: forall a. Ord a => TypeF a -> a
$cmaximum :: forall a. Ord a => TypeF a -> a
elem :: forall a. Eq a => a -> TypeF a -> Bool
$celem :: forall a. Eq a => a -> TypeF a -> Bool
length :: forall a. TypeF a -> Int
$clength :: forall a. TypeF a -> Int
null :: forall a. TypeF a -> Bool
$cnull :: forall a. TypeF a -> Bool
toList :: forall a. TypeF a -> [a]
$ctoList :: forall a. TypeF a -> [a]
foldl1 :: forall a. (a -> a -> a) -> TypeF a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TypeF a -> a
foldr1 :: forall a. (a -> a -> a) -> TypeF a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> TypeF a -> a
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
$cfoldl :: forall b a. (b -> a -> 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
$cfoldr :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
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
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
fold :: forall m. Monoid m => TypeF m -> m
$cfold :: forall m. Monoid m => TypeF m -> m
Foldable, Functor TypeF
Foldable 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)
sequence :: forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
$csequence :: forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
sequenceA :: forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
traverse :: 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)
Traversable, 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
$cto :: forall t x. Rep (TypeF t) x -> TypeF t
$cfrom :: forall t x. TypeF t -> Rep (TypeF t) x
Generic, 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
$cto1 :: forall a. Rep1 TypeF a -> TypeF a
$cfrom1 :: forall a. TypeF a -> Rep1 TypeF a
Generic1, Traversable TypeF
forall a. TypeF a -> TypeF a -> Maybe (TypeF (Either a (a, a)))
forall (t :: * -> *).
Traversable t
-> (forall a. t a -> t a -> Maybe (t (Either a (a, a))))
-> Unifiable t
zipMatch :: forall a. TypeF a -> TypeF a -> Maybe (TypeF (Either a (a, a)))
$czipMatch :: forall a. TypeF a -> TypeF a -> Maybe (TypeF (Either a (a, a)))
Unifiable, TypeF t -> DataType
TypeF t -> Constr
forall {t}. Data t => Typeable (TypeF t)
forall t. Data t => TypeF t -> DataType
forall t. Data t => TypeF t -> Constr
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 (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))
gmapMo :: 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)
gmapMp :: forall (m :: * -> *).
MonadPlus 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)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t)
gmapQi :: forall u. Int -> (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
gmapQ :: forall u. (forall d. Data d => d -> u) -> TypeF t -> [u]
$cgmapQ :: forall t u.
Data t =>
(forall d. Data d => d -> u) -> TypeF t -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeF t -> r
gmapT :: (forall b. Data b => b -> b) -> TypeF t -> TypeF t
$cgmapT :: forall t.
Data t =>
(forall b. Data b => b -> b) -> TypeF t -> TypeF t
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> 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))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (TypeF t))
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TypeF t))
dataTypeOf :: TypeF t -> DataType
$cdataTypeOf :: forall t. Data t => TypeF t -> DataType
toConstr :: TypeF t -> Constr
$ctoConstr :: forall t. Data t => TypeF t -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> 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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypeF t -> 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)
Data, forall t. FromJSON t => Value -> Parser [TypeF t]
forall t. FromJSON t => Value -> Parser (TypeF t)
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [TypeF t]
$cparseJSONList :: forall t. FromJSON t => Value -> Parser [TypeF t]
parseJSON :: Value -> Parser (TypeF t)
$cparseJSON :: forall t. FromJSON t => Value -> Parser (TypeF t)
FromJSON, forall t. ToJSON t => [TypeF t] -> Encoding
forall t. ToJSON t => [TypeF t] -> Value
forall t. ToJSON t => TypeF t -> Encoding
forall t. ToJSON t => TypeF t -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [TypeF t] -> Encoding
$ctoEncodingList :: forall t. ToJSON t => [TypeF t] -> Encoding
toJSONList :: [TypeF t] -> Value
$ctoJSONList :: forall t. ToJSON t => [TypeF t] -> Value
toEncoding :: TypeF t -> Encoding
$ctoEncoding :: forall t. ToJSON t => TypeF t -> Encoding
toJSON :: TypeF t -> Value
$ctoJSON :: forall t. ToJSON t => TypeF t -> Value
ToJSON)

-- | Unify two Maps by insisting they must have exactly the same keys,
--   and if so, simply matching up corresponding values to be
--   recursively unified.  There could be other reasonable
--   implementations, but in our case we will use this for unifying
--   record types, and we do not have any subtyping, so record types
--   will only unify if they have exactly the same keys.
instance Ord k => Unifiable (Map k) where
  zipMatch :: forall a. Map k a -> Map k a -> Maybe (Map k (Either a (a, a)))
zipMatch Map k a
m1 Map k a
m2 = do
    forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall k a. Map k a -> Set k
M.keysSet) Map k a
m1 Map k a
m2
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
M.merge forall (f :: * -> *) k x y. Applicative f => WhenMissing f k x y
M.dropMissing forall (f :: * -> *) k x y. Applicative f => WhenMissing f k x y
M.dropMissing (forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
M.zipWithMatched (\k
_ a
a1 a
a2 -> forall a b. b -> Either a b
Right (a
a1, a
a2))) Map k a
m1 Map k a
m2

-- | @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 Var
tyVars = forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
cata (\case TyVarF Var
x -> forall a. a -> Set a
S.singleton Var
x; TypeF (Set Var)
f -> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold TypeF (Set Var)
f)

-- The derived Data instance is so we can make a quasiquoter for types.
deriving instance Data Type

-- | 'UType's are like 'Type's, but also contain unification
--   variables.  'UType' is defined via 'UTerm', which is also a kind
--   of fixed point (in fact, 'UType' 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 = UTerm TypeF IntVar

-- The derived Data instances are so we can make a quasiquoter for
-- types.
deriving instance Data UType
deriving instance Data IntVar

-- | A generic /fold/ for things defined via 'UTerm' (including, in
--   particular, 'UType').  This probably belongs in the
--   @unification-fd@ package, but since it doesn't provide one, we
--   define it here.
ucata :: Functor t => (v -> a) -> (t a -> a) -> UTerm t v -> a
ucata :: forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> UTerm t v -> a
ucata v -> a
f t a -> a
_ (UVar v
v) = v -> a
f v
v
ucata v -> a
f t a -> a
g (UTerm t (UTerm t v)
t) = t a -> a
g (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> UTerm t v -> a
ucata v -> a
f t a -> a
g) t (UTerm 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 :: Var -> IntVar -> Var
mkVarName Var
nm (IntVar Int
v) = Var -> Var -> Var
T.append Var
nm (forall source target. From source target => source -> target
from @String (forall a. Show a => a -> String
show (Int
v forall a. Num a => a -> a -> a
+ (forall a. Bounded a => a
maxBound :: Int) forall a. Num a => a -> a -> a
+ Int
1)))

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

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

------------------------------------------------------------
-- 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

------------------------------------------------------------
-- 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 [Var] t
  deriving (Int -> Poly t -> ShowS
forall t. Show t => Int -> Poly t -> ShowS
forall t. Show t => [Poly t] -> ShowS
forall t. Show t => Poly t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Poly t] -> ShowS
$cshowList :: forall t. Show t => [Poly t] -> ShowS
show :: Poly t -> String
$cshow :: forall t. Show t => Poly t -> String
showsPrec :: Int -> Poly t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> Poly t -> ShowS
Show, Poly t -> Poly t -> Bool
forall t. Eq t => Poly t -> Poly t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Poly t -> Poly t -> Bool
$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
Eq, 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
<$ :: forall a b. a -> Poly b -> Poly a
$c<$ :: forall a b. a -> Poly b -> Poly a
fmap :: forall a b. (a -> b) -> Poly a -> Poly b
$cfmap :: forall a b. (a -> b) -> Poly a -> Poly b
Functor, 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
product :: forall a. Num a => Poly a -> a
$cproduct :: forall a. Num a => Poly a -> a
sum :: forall a. Num a => Poly a -> a
$csum :: forall a. Num a => Poly a -> a
minimum :: forall a. Ord a => Poly a -> a
$cminimum :: forall a. Ord a => Poly a -> a
maximum :: forall a. Ord a => Poly a -> a
$cmaximum :: forall a. Ord a => Poly a -> a
elem :: forall a. Eq a => a -> Poly a -> Bool
$celem :: forall a. Eq a => a -> Poly a -> Bool
length :: forall a. Poly a -> Int
$clength :: forall a. Poly a -> Int
null :: forall a. Poly a -> Bool
$cnull :: forall a. Poly a -> Bool
toList :: forall a. Poly a -> [a]
$ctoList :: forall a. Poly a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Poly a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Poly a -> a
foldr1 :: forall a. (a -> a -> a) -> Poly a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Poly a -> a
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
$cfoldl :: forall b a. (b -> a -> 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
$cfoldr :: forall a b. (a -> b -> b) -> b -> Poly a -> b
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
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Poly a -> m
fold :: forall m. Monoid m => Poly m -> m
$cfold :: forall m. Monoid m => Poly m -> m
Foldable, Functor Poly
Foldable 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)
sequence :: forall (m :: * -> *) a. Monad m => Poly (m a) -> m (Poly a)
$csequence :: forall (m :: * -> *) a. Monad m => Poly (m a) -> m (Poly a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Poly a -> m (Poly b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Poly a -> m (Poly b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Poly (f a) -> f (Poly a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Poly (f a) -> f (Poly a)
traverse :: 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)
Traversable, Poly t -> DataType
Poly t -> Constr
forall {t}. Data t => Typeable (Poly t)
forall t. Data t => Poly t -> DataType
forall t. Data t => Poly t -> Constr
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 (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))
gmapMo :: 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)
gmapMp :: forall (m :: * -> *).
MonadPlus 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)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Poly t -> m (Poly t)
gmapQi :: forall u. Int -> (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
gmapQ :: forall u. (forall d. Data d => d -> u) -> Poly t -> [u]
$cgmapQ :: forall t u. Data t => (forall d. Data d => d -> u) -> Poly t -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r
gmapT :: (forall b. Data b => b -> b) -> Poly t -> Poly t
$cgmapT :: forall t.
Data t =>
(forall b. Data b => b -> b) -> Poly t -> Poly t
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> 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))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Poly t))
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Poly t))
dataTypeOf :: Poly t -> DataType
$cdataTypeOf :: forall t. Data t => Poly t -> DataType
toConstr :: Poly t -> Constr
$ctoConstr :: forall t. Data t => Poly t -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> 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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Poly t -> 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)
Data, 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
$cto :: forall t x. Rep (Poly t) x -> Poly t
$cfrom :: forall t x. Poly t -> Rep (Poly t) x
Generic, forall t. FromJSON t => Value -> Parser [Poly t]
forall t. FromJSON t => Value -> Parser (Poly t)
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [Poly t]
$cparseJSONList :: forall t. FromJSON t => Value -> Parser [Poly t]
parseJSON :: Value -> Parser (Poly t)
$cparseJSON :: forall t. FromJSON t => Value -> Parser (Poly t)
FromJSON, forall t. ToJSON t => [Poly t] -> Encoding
forall t. ToJSON t => [Poly t] -> Value
forall t. ToJSON t => Poly t -> Encoding
forall t. ToJSON t => Poly t -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [Poly t] -> Encoding
$ctoEncodingList :: forall t. ToJSON t => [Poly t] -> Encoding
toJSONList :: [Poly t] -> Value
$ctoJSONList :: forall t. ToJSON t => [Poly t] -> Value
toEncoding :: Poly t -> Encoding
$ctoEncoding :: forall t. ToJSON t => Poly t -> Encoding
toJSON :: Poly t -> Value
$ctoJSON :: forall t. ToJSON t => Poly t -> Value
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 = forall (t :: * -> *) v. Functor t => Fix t -> UTerm t v
unfreeze
  fromU :: U Type -> Maybe Type
fromU = forall (t :: * -> *) v. Traversable t => UTerm t v -> Maybe (Fix t)
freeze

-- | 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. WithU t => t -> U t
toU
  fromU :: U (f t) -> Maybe (f t)
fromU = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall t. WithU t => U t -> Maybe t
fromU

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

pattern TyBase :: BaseTy -> Type
pattern $bTyBase :: BaseTy -> Type
$mTyBase :: forall {r}. Type -> (BaseTy -> r) -> ((# #) -> r) -> r
TyBase b = Fix (TyBaseF b)

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

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

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

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

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

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

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

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

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

infixr 5 :+:

pattern (:+:) :: Type -> Type -> Type
pattern ty1 $b:+: :: Type -> Type -> Type
$m:+: :: forall {r}. Type -> (Type -> Type -> r) -> ((# #) -> r) -> r
:+: ty2 = Fix (TySumF ty1 ty2)

infixr 6 :*:

pattern (:*:) :: Type -> Type -> Type
pattern ty1 $b:*: :: Type -> Type -> Type
$m:*: :: forall {r}. Type -> (Type -> Type -> r) -> ((# #) -> r) -> r
:*: ty2 = Fix (TyProdF ty1 ty2)

infixr 1 :->:

pattern (:->:) :: Type -> Type -> Type
pattern ty1 $b:->: :: Type -> Type -> Type
$m:->: :: forall {r}. Type -> (Type -> Type -> r) -> ((# #) -> r) -> r
:->: ty2 = Fix (TyFunF ty1 ty2)

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

pattern TyCmd :: Type -> Type
pattern $bTyCmd :: Type -> Type
$mTyCmd :: forall {r}. Type -> (Type -> r) -> ((# #) -> r) -> r
TyCmd ty1 = Fix (TyCmdF ty1)

pattern TyDelay :: Type -> Type
pattern $bTyDelay :: Type -> Type
$mTyDelay :: forall {r}. Type -> (Type -> r) -> ((# #) -> r) -> r
TyDelay ty1 = Fix (TyDelayF ty1)

pattern UTyBase :: BaseTy -> UType
pattern $bUTyBase :: BaseTy -> UType
$mUTyBase :: forall {r}. UType -> (BaseTy -> r) -> ((# #) -> r) -> r
UTyBase b = UTerm (TyBaseF b)

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

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

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

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

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

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

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

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

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

pattern UTySum :: UType -> UType -> UType
pattern $bUTySum :: UType -> UType -> UType
$mUTySum :: forall {r}. UType -> (UType -> UType -> r) -> ((# #) -> r) -> r
UTySum ty1 ty2 = UTerm (TySumF ty1 ty2)

pattern UTyProd :: UType -> UType -> UType
pattern $bUTyProd :: UType -> UType -> UType
$mUTyProd :: forall {r}. UType -> (UType -> UType -> r) -> ((# #) -> r) -> r
UTyProd ty1 ty2 = UTerm (TyProdF ty1 ty2)

pattern UTyFun :: UType -> UType -> UType
pattern $bUTyFun :: UType -> UType -> UType
$mUTyFun :: forall {r}. UType -> (UType -> UType -> r) -> ((# #) -> r) -> r
UTyFun ty1 ty2 = UTerm (TyFunF ty1 ty2)

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

pattern UTyCmd :: UType -> UType
pattern $bUTyCmd :: UType -> UType
$mUTyCmd :: forall {r}. UType -> (UType -> r) -> ((# #) -> r) -> r
UTyCmd ty1 = UTerm (TyCmdF ty1)

pattern UTyDelay :: UType -> UType
pattern $bUTyDelay :: UType -> UType
$mUTyDelay :: forall {r}. UType -> (UType -> r) -> ((# #) -> r) -> r
UTyDelay ty1 = UTerm (TyDelayF ty1)

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

-- Derive aeson instances for type serialization
deriving instance Generic Type
deriving instance ToJSON Type
deriving instance FromJSON Type