{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

-- |
-- 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 TyType,
  pattern (:+:),
  pattern (:*:),
  pattern (:->:),
  pattern TyRcd,
  pattern TyCmd,
  pattern TyDelay,
  pattern TyUser,
  pattern TyRec,

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

  -- ** Utilities
  ucata,
  mkVarName,
  fuvs,
  hasAnyUVars,
  isTopLevelConstructor,
  UnchainableFun (..),

  -- * Polytypes
  ImplicitQuantification (..),
  Poly,
  mkPoly,
  mkQPoly,
  mkTrivPoly,
  unPoly,
  ptVars,
  ptBody,
  Polytype,
  RawPolytype,
  pattern PolyUnit,
  UPolytype,
  quantify,
  absQuantify,
  forgetQ,

  -- * Contexts
  TCtx,
  UCtx,
  TVCtx,

  -- * User type definitions
  TydefInfo (..),
  tydefType,
  tydefArity,
  substTydef,
  ExpandTydefErr (..),
  expandTydef,
  expandTydefs,
  elimTydef,
  TDCtx,
  emptyTDCtx,
  lookupTD,
  lookupTDR,
  addBindingTD,
  withBindingTD,
  resolveUserTy,

  -- * WHNF
  whnfType,

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

import Control.Algebra (Has, run)
import Control.Carrier.Reader (runReader)
import Control.Carrier.Throw.Either (runThrow)
import Control.Effect.Reader (Reader, ask, local)
import Control.Effect.Throw (Throw, throwError)
import Control.Lens (Plated (..), makeLenses, rewriteM, view)
import Control.Monad.Free
import Data.Aeson (FromJSON (..), FromJSON1 (..), ToJSON (..), ToJSON1 (..), genericLiftParseJSON, genericLiftToJSON, genericParseJSON, genericToJSON)
import Data.Data (Data)
import Data.Data.Lens (uniplate)
import Data.Eq.Deriving (deriveEq1)
import Data.Fix
import Data.Foldable (fold)
import Data.Functor.Classes (Eq1)
import Data.Hashable (Hashable (..))
import Data.Hashable.Lifted (Hashable1)
import Data.Kind qualified
import Data.List.NonEmpty ((<|))
import Data.List.NonEmpty qualified as NE
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as M
import Data.MonoidMap (MonoidMap)
import Data.MonoidMap qualified as MM
import Data.MonoidMap.JSON ()
import Data.Ord.Deriving (deriveOrd1)
import Data.Semigroup (Sum (..))
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 Prettyprinter (align, braces, brackets, concatWith, flatAlt, hsep, pretty, punctuate, softline, (<+>))
import Swarm.Language.Context (Ctx)
import Swarm.Language.Context qualified as Ctx
import Swarm.Language.TDVar (TDVar, mkTDVar, mkTDVar', tdVarName)
import Swarm.Language.Var (Var)
import Swarm.Pretty (PrettyPrec (..), pparens, pparens', ppr, prettyBinding)
import Swarm.Util (showT, unsnocNE)
import Swarm.Util.JSON (optionsMinimize, optionsUnwrapUnary)
import Text.Show.Deriving (deriveShow1)
import Witch (into)

------------------------------------------------------------
-- 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
  | -- | The type of types
    BType
  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, Eq BaseTy
Eq BaseTy =>
(Int -> BaseTy -> Int) -> (BaseTy -> Int) -> Hashable BaseTy
Int -> BaseTy -> Int
BaseTy -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> BaseTy -> Int
hashWithSalt :: Int -> BaseTy -> Int
$chash :: BaseTy -> Int
hash :: BaseTy -> Int
Hashable, 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

instance PrettyPrec BaseTy where
  prettyPrec :: forall ann. Int -> BaseTy -> Doc ann
prettyPrec Int
_ = [Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ([Char] -> Doc ann) -> (BaseTy -> [Char]) -> BaseTy -> Doc ann
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 TDVar
  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, Eq TyCon
Eq TyCon =>
(Int -> TyCon -> Int) -> (TyCon -> Int) -> Hashable TyCon
Int -> TyCon -> Int
TyCon -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> TyCon -> Int
hashWithSalt :: Int -> TyCon -> Int
$chash :: TyCon -> Int
hash :: TyCon -> Int
Hashable)

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

instance PrettyPrec TyCon where
  prettyPrec :: forall ann. Int -> TyCon -> Doc ann
prettyPrec Int
_ = \case
    TCBase BaseTy
b -> BaseTy -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr BaseTy
b
    TyCon
TCCmd -> Doc ann
"Cmd"
    TyCon
TCDelay -> Doc ann
"Delay"
    TyCon
TCSum -> Doc ann
"Sum"
    TyCon
TCProd -> Doc ann
"Prod"
    TyCon
TCFun -> Doc ann
"Fun"
    TCUser TDVar
t -> TDVar -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TDVar
t

-- | 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, Eq Arity
Eq Arity =>
(Int -> Arity -> Int) -> (Arity -> Int) -> Hashable Arity
Int -> Arity -> Int
Arity -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> Arity -> Int
hashWithSalt :: Int -> Arity -> Int
$chash :: Arity -> Int
hash :: Arity -> Int
Hashable)

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

instance PrettyPrec Arity where
  prettyPrec :: forall ann. Int -> Arity -> Doc ann
prettyPrec Int
_ (Arity Int
a) = Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
a

------------------------------------------------------------
-- 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, Eq Nat
Eq Nat => (Int -> Nat -> Int) -> (Nat -> Int) -> Hashable Nat
Int -> Nat -> Int
Nat -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> Nat -> Int
hashWithSalt :: Int -> Nat -> Int
$chash :: Nat -> Int
hash :: Nat -> Int
Hashable, 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.  The first Var represents the original name,
    --   and should be ignored except for use in e.g. error messages.
    --   The second Var is the real name of the variable; it may be the
    --   same as the first, or it may be different e.g. if it is a
    --   freshly generated skolem variable.
    TyVarF Var 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, Eq (TypeF t)
Eq (TypeF t) =>
(Int -> TypeF t -> Int) -> (TypeF t -> Int) -> Hashable (TypeF t)
Int -> TypeF t -> Int
TypeF t -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall t. Hashable t => Eq (TypeF t)
forall t. Hashable t => Int -> TypeF t -> Int
forall t. Hashable t => TypeF t -> Int
$chashWithSalt :: forall t. Hashable t => Int -> TypeF t -> Int
hashWithSalt :: Int -> TypeF t -> Int
$chash :: forall t. Hashable t => TypeF t -> Int
hash :: TypeF t -> Int
Hashable)

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

instance Hashable1 TypeF -- needs the Eq1 instance

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

instance Plated Type where
  plate :: Traversal' Type Type
plate = (Type -> f Type) -> Type -> f Type
forall a. Data a => Traversal' a a
Traversal' Type Type
uniplate

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, (forall x. IntVar -> Rep IntVar x)
-> (forall x. Rep IntVar x -> IntVar) -> Generic IntVar
forall x. Rep IntVar x -> IntVar
forall x. IntVar -> Rep IntVar x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. IntVar -> Rep IntVar x
from :: forall x. IntVar -> Rep IntVar x
$cto :: forall x. Rep IntVar x -> IntVar
to :: forall x. Rep IntVar x -> IntVar
Generic, Eq IntVar
Eq IntVar =>
(Int -> IntVar -> Int) -> (IntVar -> Int) -> Hashable IntVar
Int -> IntVar -> Int
IntVar -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> IntVar -> Int
hashWithSalt :: Int -> IntVar -> Int
$chash :: IntVar -> Int
hash :: IntVar -> Int
Hashable)

instance PrettyPrec IntVar where
  prettyPrec :: forall ann. Int -> IntVar -> Doc ann
prettyPrec Int
_ = Text -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr (Text -> Doc ann) -> (IntVar -> Text) -> IntVar -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> IntVar -> Text
mkVarName Text
"u"

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

-- orphan instance
instance (Eq1 f, Hashable x, Hashable (f (Free f x))) => Hashable (Free f x)

-- | 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 (Int -> Text
forall a. Show a => a -> Text
showT 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

-- | Check whether a type contains any unification variables at all.
hasAnyUVars :: UType -> Bool
hasAnyUVars :: UType -> Bool
hasAnyUVars = (IntVar -> Bool) -> (TypeF Bool -> Bool) -> UType -> Bool
forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> Free t v -> a
ucata (Bool -> IntVar -> Bool
forall a b. a -> b -> a
const Bool
True) TypeF Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or

-- | Check whether a type consists of a top-level type constructor
--   immediately applied to unification variables.
isTopLevelConstructor :: UType -> Maybe (TypeF ())
isTopLevelConstructor :: UType -> Maybe (TypeF ())
isTopLevelConstructor = \case
  Free (TyRcdF Map Text UType
m) | (UType -> Bool) -> Map Text UType -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all UType -> Bool
forall (f :: * -> *) a. Free f a -> Bool
isPure Map Text UType
m -> TypeF () -> Maybe (TypeF ())
forall a. a -> Maybe a
Just (Map Text () -> TypeF ()
forall t. Map Text t -> TypeF t
TyRcdF Map Text ()
forall k a. Map k a
M.empty)
  UTyConApp TyCon
c [UType]
ts | (UType -> Bool) -> [UType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all UType -> Bool
forall (f :: * -> *) a. Free f a -> Bool
isPure [UType]
ts -> TypeF () -> Maybe (TypeF ())
forall a. a -> Maybe a
Just (TyCon -> [()] -> TypeF ()
forall t. TyCon -> [t] -> TypeF t
TyConF TyCon
c [])
  UType
_ -> Maybe (TypeF ())
forall a. Maybe a
Nothing

isPure :: Free f a -> Bool
isPure :: forall (f :: * -> *) a. Free f a -> Bool
isPure (Pure {}) = Bool
True
isPure Free f a
_ = Bool
False

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

instance IsString UType where
  fromString :: [Char] -> UType
fromString = Text -> UType
UTyVar (Text -> UType) -> ([Char] -> Text) -> [Char] -> UType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall target source. From source target => source -> target
into @Text

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

--------------------------------------------------
-- Pretty-printing machinery for types

-- | Split a function type chain, so that we can pretty print
--   the type parameters aligned on each line when they don't fit.
class UnchainableFun t where
  unchainFun :: t -> NE.NonEmpty t

instance UnchainableFun Type where
  unchainFun :: Type -> NonEmpty Type
unchainFun (Type
a :->: Type
ty) = Type
a Type -> NonEmpty Type -> NonEmpty Type
forall a. a -> NonEmpty a -> NonEmpty a
<| Type -> NonEmpty Type
forall t. UnchainableFun t => t -> NonEmpty t
unchainFun Type
ty
  unchainFun Type
ty = Type -> NonEmpty Type
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty

instance UnchainableFun (Free TypeF ty) where
  unchainFun :: Free TypeF ty -> NonEmpty (Free TypeF ty)
unchainFun (Free (TyConF TyCon
TCFun [Free TypeF ty
ty1, Free TypeF ty
ty2])) = Free TypeF ty
ty1 Free TypeF ty
-> NonEmpty (Free TypeF ty) -> NonEmpty (Free TypeF ty)
forall a. a -> NonEmpty a -> NonEmpty a
<| Free TypeF ty -> NonEmpty (Free TypeF ty)
forall t. UnchainableFun t => t -> NonEmpty t
unchainFun Free TypeF ty
ty2
  unchainFun Free TypeF ty
ty = Free TypeF ty -> NonEmpty (Free TypeF ty)
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Free TypeF ty
ty

instance (UnchainableFun t, PrettyPrec t, SubstRec t) => PrettyPrec (TypeF t) where
  prettyPrec :: forall ann. Int -> TypeF t -> Doc ann
prettyPrec Int
p = \case
    TyVarF Text
v Text
_ -> Text -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Text
v
    TyRcdF Map Text t
m -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep (Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
"," (((Text, t) -> Doc ann) -> [(Text, t)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Text, t) -> Doc ann
forall a b ann. (PrettyPrec a, PrettyPrec b) => (a, b) -> Doc ann
prettyBinding (Map Text t -> [(Text, t)]
forall k a. Map k a -> [(k, a)]
M.assocs Map Text t
m)))
    -- Special cases for type constructors with special syntax.
    -- Always use parentheses around sum and product types, see #1625
    TyConF TyCon
TCSum [t
ty1, t
ty2] ->
      Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
        Int -> t -> Doc ann
forall ann. Int -> t -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
2 t
ty1 Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"+" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> t -> Doc ann
forall ann. Int -> t -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
2 t
ty2
    TyConF TyCon
TCProd [t
ty1, t
ty2] ->
      Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
        Int -> t -> Doc ann
forall ann. Int -> t -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
2 t
ty1 Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"*" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> t -> Doc ann
forall ann. Int -> t -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
2 t
ty2
    TyConF TyCon
TCDelay [t
ty] -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
braces (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ t -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr t
ty
    TyConF TyCon
TCFun [t
ty1, t
ty2] ->
      let ([t]
iniF, t
lastF) = NonEmpty t -> ([t], t)
forall a. NonEmpty a -> ([a], a)
unsnocNE (NonEmpty t -> ([t], t)) -> NonEmpty t -> ([t], t)
forall a b. (a -> b) -> a -> b
$ t
ty1 t -> NonEmpty t -> NonEmpty t
forall a. a -> NonEmpty a -> NonEmpty a
<| t -> NonEmpty t
forall t. UnchainableFun t => t -> NonEmpty t
unchainFun t
ty2
          funs :: [Doc ann]
funs = (Int -> t -> Doc ann
forall ann. Int -> t -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
2 (t -> Doc ann) -> [t] -> [Doc ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [t]
iniF) [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. Semigroup a => a -> a -> a
<> [Int -> t -> Doc ann
forall ann. Int -> t -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
1 t
lastF]
          inLine :: Doc ann -> Doc ann -> Doc ann
inLine Doc ann
l Doc ann
r = Doc ann
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"->" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
r
          multiLine :: Doc ann -> Doc ann -> Doc ann
multiLine Doc ann
l Doc ann
r = Doc ann
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"->" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
softline Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
r
       in Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens' (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (Doc ann -> Doc ann) -> (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
            Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
flatAlt ((Doc ann -> Doc ann -> Doc ann) -> [Doc ann] -> Doc ann
forall (t :: * -> *) ann.
Foldable t =>
(Doc ann -> Doc ann -> Doc ann) -> t (Doc ann) -> Doc ann
concatWith Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
multiLine [Doc ann]
funs) ((Doc ann -> Doc ann -> Doc ann) -> [Doc ann] -> Doc ann
forall (t :: * -> *) ann.
Foldable t =>
(Doc ann -> Doc ann -> Doc ann) -> t (Doc ann) -> Doc ann
concatWith Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
inLine [Doc ann]
funs)
    TyRecF Text
x t
ty ->
      Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
        Doc ann
"rec" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Text
x Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"." Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> t -> Doc ann
forall ann. Int -> t -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
0 (TypeF t -> t -> Nat -> t
forall t. SubstRec t => TypeF t -> t -> Nat -> t
substRec (Text -> Text -> TypeF t
forall t. Text -> Text -> TypeF t
TyVarF Text
x Text
x) t
ty Nat
NZ)
    -- This case shouldn't be possible, since TyRecVar should only occur inside a TyRec,
    -- and pretty-printing the TyRec (above) will substitute a variable name for
    -- any bound TyRecVars before recursing.
    TyRecVarF Nat
i -> [Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Int -> [Char]
forall a. Show a => a -> [Char]
show (Nat -> Int
natToInt Nat
i))
    -- Fallthrough cases for type constructor application.  Handles base
    -- types, Cmd, user-defined types, or ill-kinded things like 'Int
    -- Bool'.
    TyConF TyCon
c [] -> TyCon -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TyCon
c
    TyConF TyCon
c [t]
tys -> Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ TyCon -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TyCon
c Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ((t -> Doc ann) -> [t] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> t -> Doc ann
forall ann. Int -> t -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
10) [t]
tys)

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

-- | Type class for various type representations (e.g. 'Type',
--   'UType') and generic operations we can perform on them.  This
--   helps us avoid code duplication in some cases, by writing a
--   single generic function which works for any 'Typical' instance.
class Typical t where
  -- | Fold a type into a summary value of some type @a@, given an
  --   "empty" value of type @a@ (for use at e.g. Pure nodes in a
  --   UType)
  foldT :: a -> (TypeF a -> a) -> t -> a

  -- | Refold a type into another type.  This is a special case of
  --   'foldT' when we want to produce another type, since then we can
  --   do something more sensible with 'Pure' nodes in a 'UType'
  --   (i.e. preserve them instead of replacing them with a default
  --   value).
  refoldT :: (TypeF t -> t) -> t -> t

  -- | Unroll one level of structure.
  unrollT :: t -> Maybe (TypeF t)

  -- | Roll up one level of structure.
  rollT :: TypeF t -> t

  -- | It should be possible to convert 'Type' to any type-ish thing.
  fromType :: Type -> t

instance Typical Type where
  foldT :: forall a. a -> (TypeF a -> a) -> Type -> a
foldT a
_ = (TypeF a -> a) -> Type -> a
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix
  refoldT :: (TypeF Type -> Type) -> Type -> Type
refoldT = (TypeF Type -> Type) -> Type -> Type
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix
  unrollT :: Type -> Maybe (TypeF Type)
unrollT (Fix TypeF Type
t) = TypeF Type -> Maybe (TypeF Type)
forall a. a -> Maybe a
Just TypeF Type
t
  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 :: forall a. a -> (TypeF a -> a) -> UType -> a
foldT a
e = (IntVar -> a) -> (TypeF a -> a) -> UType -> a
forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> Free t v -> a
ucata (a -> IntVar -> a
forall a b. a -> b -> a
const a
e)
  refoldT :: (TypeF UType -> UType) -> UType -> UType
refoldT = (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
  unrollT :: UType -> Maybe (TypeF UType)
unrollT (Free TypeF UType
t) = TypeF UType -> Maybe (TypeF UType)
forall a. a -> Maybe a
Just TypeF UType
t
  unrollT UType
_ = Maybe (TypeF UType)
forall a. Maybe a
Nothing
  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

-- | Get all the type variables (/not/ unification variables)
--   contained in a 'Type' or 'UType'.
tyVars :: Typical t => t -> Set Var
tyVars :: forall t. Typical t => t -> Set Text
tyVars = Set Text -> (TypeF (Set Text) -> Set Text) -> t -> Set Text
forall a. a -> (TypeF a -> a) -> t -> a
forall t a. Typical t => a -> (TypeF a -> a) -> t -> a
foldT Set Text
forall a. Set a
S.empty (\case TyVarF Text
_ 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)

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

data ImplicitQuantification = Unquantified | Quantified
  deriving (ImplicitQuantification -> ImplicitQuantification -> Bool
(ImplicitQuantification -> ImplicitQuantification -> Bool)
-> (ImplicitQuantification -> ImplicitQuantification -> Bool)
-> Eq ImplicitQuantification
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ImplicitQuantification -> ImplicitQuantification -> Bool
== :: ImplicitQuantification -> ImplicitQuantification -> Bool
$c/= :: ImplicitQuantification -> ImplicitQuantification -> Bool
/= :: ImplicitQuantification -> ImplicitQuantification -> Bool
Eq, Eq ImplicitQuantification
Eq ImplicitQuantification =>
(ImplicitQuantification -> ImplicitQuantification -> Ordering)
-> (ImplicitQuantification -> ImplicitQuantification -> Bool)
-> (ImplicitQuantification -> ImplicitQuantification -> Bool)
-> (ImplicitQuantification -> ImplicitQuantification -> Bool)
-> (ImplicitQuantification -> ImplicitQuantification -> Bool)
-> (ImplicitQuantification
    -> ImplicitQuantification -> ImplicitQuantification)
-> (ImplicitQuantification
    -> ImplicitQuantification -> ImplicitQuantification)
-> Ord ImplicitQuantification
ImplicitQuantification -> ImplicitQuantification -> Bool
ImplicitQuantification -> ImplicitQuantification -> Ordering
ImplicitQuantification
-> ImplicitQuantification -> ImplicitQuantification
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 :: ImplicitQuantification -> ImplicitQuantification -> Ordering
compare :: ImplicitQuantification -> ImplicitQuantification -> Ordering
$c< :: ImplicitQuantification -> ImplicitQuantification -> Bool
< :: ImplicitQuantification -> ImplicitQuantification -> Bool
$c<= :: ImplicitQuantification -> ImplicitQuantification -> Bool
<= :: ImplicitQuantification -> ImplicitQuantification -> Bool
$c> :: ImplicitQuantification -> ImplicitQuantification -> Bool
> :: ImplicitQuantification -> ImplicitQuantification -> Bool
$c>= :: ImplicitQuantification -> ImplicitQuantification -> Bool
>= :: ImplicitQuantification -> ImplicitQuantification -> Bool
$cmax :: ImplicitQuantification
-> ImplicitQuantification -> ImplicitQuantification
max :: ImplicitQuantification
-> ImplicitQuantification -> ImplicitQuantification
$cmin :: ImplicitQuantification
-> ImplicitQuantification -> ImplicitQuantification
min :: ImplicitQuantification
-> ImplicitQuantification -> ImplicitQuantification
Ord, ReadPrec [ImplicitQuantification]
ReadPrec ImplicitQuantification
Int -> ReadS ImplicitQuantification
ReadS [ImplicitQuantification]
(Int -> ReadS ImplicitQuantification)
-> ReadS [ImplicitQuantification]
-> ReadPrec ImplicitQuantification
-> ReadPrec [ImplicitQuantification]
-> Read ImplicitQuantification
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS ImplicitQuantification
readsPrec :: Int -> ReadS ImplicitQuantification
$creadList :: ReadS [ImplicitQuantification]
readList :: ReadS [ImplicitQuantification]
$creadPrec :: ReadPrec ImplicitQuantification
readPrec :: ReadPrec ImplicitQuantification
$creadListPrec :: ReadPrec [ImplicitQuantification]
readListPrec :: ReadPrec [ImplicitQuantification]
Read, Int -> ImplicitQuantification -> ShowS
[ImplicitQuantification] -> ShowS
ImplicitQuantification -> [Char]
(Int -> ImplicitQuantification -> ShowS)
-> (ImplicitQuantification -> [Char])
-> ([ImplicitQuantification] -> ShowS)
-> Show ImplicitQuantification
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ImplicitQuantification -> ShowS
showsPrec :: Int -> ImplicitQuantification -> ShowS
$cshow :: ImplicitQuantification -> [Char]
show :: ImplicitQuantification -> [Char]
$cshowList :: [ImplicitQuantification] -> ShowS
showList :: [ImplicitQuantification] -> ShowS
Show)

-- | A @Poly q 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")@.
--
--   The type index @q@ is a phantom type index indicating whether the
--   type has been implicitly quantified.  Immediately after a
--   polytype is parsed it is 'Unquantified' and unsafe to use.  For
--   example, the type @a -> a@ would parse literally as @Forall []
--   (TyFun "a" "a") :: Poly Unquantified Type@, where the type
--   variable @a@ is not in the list of bound variables.  Later, after
--   running through 'quantify', it would become a @Poly Quantified
--   Type@, either @Forall ["a"] (TyFun "a" "a")@ if the type variable
--   is implicitly quantified, or unchanged if the type variable @a@
--   was already in scope.
--
--   The @Poly@ constructor intentionally unexported, so that the
--   only way to create a @Poly Quantified@ is through the 'quantify'
--   function.
data Poly (q :: ImplicitQuantification) t = Forall {forall (q :: ImplicitQuantification) t. Poly q t -> [Text]
_ptVars :: [Var], forall (q :: ImplicitQuantification) t. Poly q t -> t
ptBody :: t}
  deriving (Int -> Poly q t -> ShowS
[Poly q t] -> ShowS
Poly q t -> [Char]
(Int -> Poly q t -> ShowS)
-> (Poly q t -> [Char]) -> ([Poly q t] -> ShowS) -> Show (Poly q t)
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
forall (q :: ImplicitQuantification) t.
Show t =>
Int -> Poly q t -> ShowS
forall (q :: ImplicitQuantification) t.
Show t =>
[Poly q t] -> ShowS
forall (q :: ImplicitQuantification) t.
Show t =>
Poly q t -> [Char]
$cshowsPrec :: forall (q :: ImplicitQuantification) t.
Show t =>
Int -> Poly q t -> ShowS
showsPrec :: Int -> Poly q t -> ShowS
$cshow :: forall (q :: ImplicitQuantification) t.
Show t =>
Poly q t -> [Char]
show :: Poly q t -> [Char]
$cshowList :: forall (q :: ImplicitQuantification) t.
Show t =>
[Poly q t] -> ShowS
showList :: [Poly q t] -> ShowS
Show, Poly q t -> Poly q t -> Bool
(Poly q t -> Poly q t -> Bool)
-> (Poly q t -> Poly q t -> Bool) -> Eq (Poly q t)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (q :: ImplicitQuantification) t.
Eq t =>
Poly q t -> Poly q t -> Bool
$c== :: forall (q :: ImplicitQuantification) t.
Eq t =>
Poly q t -> Poly q t -> Bool
== :: Poly q t -> Poly q t -> Bool
$c/= :: forall (q :: ImplicitQuantification) t.
Eq t =>
Poly q t -> Poly q t -> Bool
/= :: Poly q t -> Poly q t -> Bool
Eq, (forall a b. (a -> b) -> Poly q a -> Poly q b)
-> (forall a b. a -> Poly q b -> Poly q a) -> Functor (Poly q)
forall a b. a -> Poly q b -> Poly q a
forall a b. (a -> b) -> Poly q a -> Poly q b
forall (q :: ImplicitQuantification) a b. a -> Poly q b -> Poly q a
forall (q :: ImplicitQuantification) a b.
(a -> b) -> Poly q a -> Poly q b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (q :: ImplicitQuantification) a b.
(a -> b) -> Poly q a -> Poly q b
fmap :: forall a b. (a -> b) -> Poly q a -> Poly q b
$c<$ :: forall (q :: ImplicitQuantification) a b. a -> Poly q b -> Poly q a
<$ :: forall a b. a -> Poly q b -> Poly q a
Functor, (forall m. Monoid m => Poly q m -> m)
-> (forall m a. Monoid m => (a -> m) -> Poly q a -> m)
-> (forall m a. Monoid m => (a -> m) -> Poly q a -> m)
-> (forall a b. (a -> b -> b) -> b -> Poly q a -> b)
-> (forall a b. (a -> b -> b) -> b -> Poly q a -> b)
-> (forall b a. (b -> a -> b) -> b -> Poly q a -> b)
-> (forall b a. (b -> a -> b) -> b -> Poly q a -> b)
-> (forall a. (a -> a -> a) -> Poly q a -> a)
-> (forall a. (a -> a -> a) -> Poly q a -> a)
-> (forall a. Poly q a -> [a])
-> (forall a. Poly q a -> Bool)
-> (forall a. Poly q a -> Int)
-> (forall a. Eq a => a -> Poly q a -> Bool)
-> (forall a. Ord a => Poly q a -> a)
-> (forall a. Ord a => Poly q a -> a)
-> (forall a. Num a => Poly q a -> a)
-> (forall a. Num a => Poly q a -> a)
-> Foldable (Poly q)
forall a. Eq a => a -> Poly q a -> Bool
forall a. Num a => Poly q a -> a
forall a. Ord a => Poly q a -> a
forall m. Monoid m => Poly q m -> m
forall a. Poly q a -> Bool
forall a. Poly q a -> Int
forall a. Poly q a -> [a]
forall a. (a -> a -> a) -> Poly q a -> a
forall m a. Monoid m => (a -> m) -> Poly q a -> m
forall b a. (b -> a -> b) -> b -> Poly q a -> b
forall a b. (a -> b -> b) -> b -> Poly q a -> b
forall (q :: ImplicitQuantification) a.
Eq a =>
a -> Poly q a -> Bool
forall (q :: ImplicitQuantification) a. Num a => Poly q a -> a
forall (q :: ImplicitQuantification) a. Ord a => Poly q a -> a
forall (q :: ImplicitQuantification) m. Monoid m => Poly q m -> m
forall (q :: ImplicitQuantification) a. Poly q a -> Bool
forall (q :: ImplicitQuantification) a. Poly q a -> Int
forall (q :: ImplicitQuantification) a. Poly q a -> [a]
forall (q :: ImplicitQuantification) a.
(a -> a -> a) -> Poly q a -> a
forall (q :: ImplicitQuantification) m a.
Monoid m =>
(a -> m) -> Poly q a -> m
forall (q :: ImplicitQuantification) b a.
(b -> a -> b) -> b -> Poly q a -> b
forall (q :: ImplicitQuantification) a b.
(a -> b -> b) -> b -> Poly q 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 (q :: ImplicitQuantification) m. Monoid m => Poly q m -> m
fold :: forall m. Monoid m => Poly q m -> m
$cfoldMap :: forall (q :: ImplicitQuantification) m a.
Monoid m =>
(a -> m) -> Poly q a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Poly q a -> m
$cfoldMap' :: forall (q :: ImplicitQuantification) m a.
Monoid m =>
(a -> m) -> Poly q a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Poly q a -> m
$cfoldr :: forall (q :: ImplicitQuantification) a b.
(a -> b -> b) -> b -> Poly q a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Poly q a -> b
$cfoldr' :: forall (q :: ImplicitQuantification) a b.
(a -> b -> b) -> b -> Poly q a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Poly q a -> b
$cfoldl :: forall (q :: ImplicitQuantification) b a.
(b -> a -> b) -> b -> Poly q a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Poly q a -> b
$cfoldl' :: forall (q :: ImplicitQuantification) b a.
(b -> a -> b) -> b -> Poly q a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Poly q a -> b
$cfoldr1 :: forall (q :: ImplicitQuantification) a.
(a -> a -> a) -> Poly q a -> a
foldr1 :: forall a. (a -> a -> a) -> Poly q a -> a
$cfoldl1 :: forall (q :: ImplicitQuantification) a.
(a -> a -> a) -> Poly q a -> a
foldl1 :: forall a. (a -> a -> a) -> Poly q a -> a
$ctoList :: forall (q :: ImplicitQuantification) a. Poly q a -> [a]
toList :: forall a. Poly q a -> [a]
$cnull :: forall (q :: ImplicitQuantification) a. Poly q a -> Bool
null :: forall a. Poly q a -> Bool
$clength :: forall (q :: ImplicitQuantification) a. Poly q a -> Int
length :: forall a. Poly q a -> Int
$celem :: forall (q :: ImplicitQuantification) a.
Eq a =>
a -> Poly q a -> Bool
elem :: forall a. Eq a => a -> Poly q a -> Bool
$cmaximum :: forall (q :: ImplicitQuantification) a. Ord a => Poly q a -> a
maximum :: forall a. Ord a => Poly q a -> a
$cminimum :: forall (q :: ImplicitQuantification) a. Ord a => Poly q a -> a
minimum :: forall a. Ord a => Poly q a -> a
$csum :: forall (q :: ImplicitQuantification) a. Num a => Poly q a -> a
sum :: forall a. Num a => Poly q a -> a
$cproduct :: forall (q :: ImplicitQuantification) a. Num a => Poly q a -> a
product :: forall a. Num a => Poly q a -> a
Foldable, Functor (Poly q)
Foldable (Poly q)
(Functor (Poly q), Foldable (Poly q)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Poly q a -> f (Poly q b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Poly q (f a) -> f (Poly q a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Poly q a -> m (Poly q b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Poly q (m a) -> m (Poly q a))
-> Traversable (Poly q)
forall (q :: ImplicitQuantification). Functor (Poly q)
forall (q :: ImplicitQuantification). Foldable (Poly q)
forall (q :: ImplicitQuantification) (m :: * -> *) a.
Monad m =>
Poly q (m a) -> m (Poly q a)
forall (q :: ImplicitQuantification) (f :: * -> *) a.
Applicative f =>
Poly q (f a) -> f (Poly q a)
forall (q :: ImplicitQuantification) (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Poly q a -> m (Poly q b)
forall (q :: ImplicitQuantification) (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Poly q a -> f (Poly q b)
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 q (m a) -> m (Poly q a)
forall (f :: * -> *) a.
Applicative f =>
Poly q (f a) -> f (Poly q a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Poly q a -> m (Poly q b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Poly q a -> f (Poly q b)
$ctraverse :: forall (q :: ImplicitQuantification) (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Poly q a -> f (Poly q b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Poly q a -> f (Poly q b)
$csequenceA :: forall (q :: ImplicitQuantification) (f :: * -> *) a.
Applicative f =>
Poly q (f a) -> f (Poly q a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Poly q (f a) -> f (Poly q a)
$cmapM :: forall (q :: ImplicitQuantification) (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Poly q a -> m (Poly q b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Poly q a -> m (Poly q b)
$csequence :: forall (q :: ImplicitQuantification) (m :: * -> *) a.
Monad m =>
Poly q (m a) -> m (Poly q a)
sequence :: forall (m :: * -> *) a. Monad m => Poly q (m a) -> m (Poly q a)
Traversable, Typeable (Poly q t)
Typeable (Poly q t) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Poly q t -> c (Poly q t))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Poly q t))
-> (Poly q t -> Constr)
-> (Poly q t -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Poly q t)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Poly q t)))
-> ((forall b. Data b => b -> b) -> Poly q t -> Poly q t)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Poly q t -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Poly q t -> r)
-> (forall u. (forall d. Data d => d -> u) -> Poly q t -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Poly q t -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Poly q t -> m (Poly q t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Poly q t -> m (Poly q t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Poly q t -> m (Poly q t))
-> Data (Poly q t)
Poly q t -> Constr
Poly q t -> DataType
(forall b. Data b => b -> b) -> Poly q t -> Poly q 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 q t -> u
forall u. (forall d. Data d => d -> u) -> Poly q t -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Poly q t -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Poly q t -> r
forall (q :: ImplicitQuantification) t.
(Typeable q, Data t) =>
Typeable (Poly q t)
forall (q :: ImplicitQuantification) t.
(Typeable q, Data t) =>
Poly q t -> Constr
forall (q :: ImplicitQuantification) t.
(Typeable q, Data t) =>
Poly q t -> DataType
forall (q :: ImplicitQuantification) t.
(Typeable q, Data t) =>
(forall b. Data b => b -> b) -> Poly q t -> Poly q t
forall (q :: ImplicitQuantification) t u.
(Typeable q, Data t) =>
Int -> (forall d. Data d => d -> u) -> Poly q t -> u
forall (q :: ImplicitQuantification) t u.
(Typeable q, Data t) =>
(forall d. Data d => d -> u) -> Poly q t -> [u]
forall (q :: ImplicitQuantification) t r r'.
(Typeable q, Data t) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Poly q t -> r
forall (q :: ImplicitQuantification) t r r'.
(Typeable q, Data t) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Poly q t -> r
forall (q :: ImplicitQuantification) t (m :: * -> *).
(Typeable q, Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Poly q t -> m (Poly q t)
forall (q :: ImplicitQuantification) t (m :: * -> *).
(Typeable q, Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Poly q t -> m (Poly q t)
forall (q :: ImplicitQuantification) t (c :: * -> *).
(Typeable q, Data t) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Poly q t)
forall (q :: ImplicitQuantification) t (c :: * -> *).
(Typeable q, Data t) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Poly q t -> c (Poly q t)
forall (q :: ImplicitQuantification) t (t :: * -> *) (c :: * -> *).
(Typeable q, Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Poly q t))
forall (q :: ImplicitQuantification) t (t :: * -> * -> *)
       (c :: * -> *).
(Typeable q, Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Poly q t))
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Poly q t -> m (Poly q t)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Poly q t -> m (Poly q t)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Poly q t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Poly q t -> c (Poly q t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Poly q t))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Poly q t))
$cgfoldl :: forall (q :: ImplicitQuantification) t (c :: * -> *).
(Typeable q, Data t) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Poly q t -> c (Poly q t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Poly q t -> c (Poly q t)
$cgunfold :: forall (q :: ImplicitQuantification) t (c :: * -> *).
(Typeable q, Data t) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Poly q t)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Poly q t)
$ctoConstr :: forall (q :: ImplicitQuantification) t.
(Typeable q, Data t) =>
Poly q t -> Constr
toConstr :: Poly q t -> Constr
$cdataTypeOf :: forall (q :: ImplicitQuantification) t.
(Typeable q, Data t) =>
Poly q t -> DataType
dataTypeOf :: Poly q t -> DataType
$cdataCast1 :: forall (q :: ImplicitQuantification) t (t :: * -> *) (c :: * -> *).
(Typeable q, Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Poly q t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Poly q t))
$cdataCast2 :: forall (q :: ImplicitQuantification) t (t :: * -> * -> *)
       (c :: * -> *).
(Typeable q, Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Poly q t))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Poly q t))
$cgmapT :: forall (q :: ImplicitQuantification) t.
(Typeable q, Data t) =>
(forall b. Data b => b -> b) -> Poly q t -> Poly q t
gmapT :: (forall b. Data b => b -> b) -> Poly q t -> Poly q t
$cgmapQl :: forall (q :: ImplicitQuantification) t r r'.
(Typeable q, Data t) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Poly q t -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Poly q t -> r
$cgmapQr :: forall (q :: ImplicitQuantification) t r r'.
(Typeable q, Data t) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Poly q t -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Poly q t -> r
$cgmapQ :: forall (q :: ImplicitQuantification) t u.
(Typeable q, Data t) =>
(forall d. Data d => d -> u) -> Poly q t -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Poly q t -> [u]
$cgmapQi :: forall (q :: ImplicitQuantification) t u.
(Typeable q, Data t) =>
Int -> (forall d. Data d => d -> u) -> Poly q t -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Poly q t -> u
$cgmapM :: forall (q :: ImplicitQuantification) t (m :: * -> *).
(Typeable q, Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Poly q t -> m (Poly q t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Poly q t -> m (Poly q t)
$cgmapMp :: forall (q :: ImplicitQuantification) t (m :: * -> *).
(Typeable q, Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Poly q t -> m (Poly q t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Poly q t -> m (Poly q t)
$cgmapMo :: forall (q :: ImplicitQuantification) t (m :: * -> *).
(Typeable q, Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Poly q t -> m (Poly q t)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Poly q t -> m (Poly q t)
Data, (forall x. Poly q t -> Rep (Poly q t) x)
-> (forall x. Rep (Poly q t) x -> Poly q t) -> Generic (Poly q t)
forall x. Rep (Poly q t) x -> Poly q t
forall x. Poly q t -> Rep (Poly q t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (q :: ImplicitQuantification) t x.
Rep (Poly q t) x -> Poly q t
forall (q :: ImplicitQuantification) t x.
Poly q t -> Rep (Poly q t) x
$cfrom :: forall (q :: ImplicitQuantification) t x.
Poly q t -> Rep (Poly q t) x
from :: forall x. Poly q t -> Rep (Poly q t) x
$cto :: forall (q :: ImplicitQuantification) t x.
Rep (Poly q t) x -> Poly q t
to :: forall x. Rep (Poly q t) x -> Poly q t
Generic, Maybe (Poly q t)
Value -> Parser [Poly q t]
Value -> Parser (Poly q t)
(Value -> Parser (Poly q t))
-> (Value -> Parser [Poly q t])
-> Maybe (Poly q t)
-> FromJSON (Poly q t)
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
forall (q :: ImplicitQuantification) t.
FromJSON t =>
Maybe (Poly q t)
forall (q :: ImplicitQuantification) t.
FromJSON t =>
Value -> Parser [Poly q t]
forall (q :: ImplicitQuantification) t.
FromJSON t =>
Value -> Parser (Poly q t)
$cparseJSON :: forall (q :: ImplicitQuantification) t.
FromJSON t =>
Value -> Parser (Poly q t)
parseJSON :: Value -> Parser (Poly q t)
$cparseJSONList :: forall (q :: ImplicitQuantification) t.
FromJSON t =>
Value -> Parser [Poly q t]
parseJSONList :: Value -> Parser [Poly q t]
$comittedField :: forall (q :: ImplicitQuantification) t.
FromJSON t =>
Maybe (Poly q t)
omittedField :: Maybe (Poly q t)
FromJSON, [Poly q t] -> Value
[Poly q t] -> Encoding
Poly q t -> Bool
Poly q t -> Value
Poly q t -> Encoding
(Poly q t -> Value)
-> (Poly q t -> Encoding)
-> ([Poly q t] -> Value)
-> ([Poly q t] -> Encoding)
-> (Poly q t -> Bool)
-> ToJSON (Poly q t)
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
forall (q :: ImplicitQuantification) t.
ToJSON t =>
[Poly q t] -> Value
forall (q :: ImplicitQuantification) t.
ToJSON t =>
[Poly q t] -> Encoding
forall (q :: ImplicitQuantification) t.
ToJSON t =>
Poly q t -> Bool
forall (q :: ImplicitQuantification) t.
ToJSON t =>
Poly q t -> Value
forall (q :: ImplicitQuantification) t.
ToJSON t =>
Poly q t -> Encoding
$ctoJSON :: forall (q :: ImplicitQuantification) t.
ToJSON t =>
Poly q t -> Value
toJSON :: Poly q t -> Value
$ctoEncoding :: forall (q :: ImplicitQuantification) t.
ToJSON t =>
Poly q t -> Encoding
toEncoding :: Poly q t -> Encoding
$ctoJSONList :: forall (q :: ImplicitQuantification) t.
ToJSON t =>
[Poly q t] -> Value
toJSONList :: [Poly q t] -> Value
$ctoEncodingList :: forall (q :: ImplicitQuantification) t.
ToJSON t =>
[Poly q t] -> Encoding
toEncodingList :: [Poly q t] -> Encoding
$comitField :: forall (q :: ImplicitQuantification) t.
ToJSON t =>
Poly q t -> Bool
omitField :: Poly q t -> Bool
ToJSON, Eq (Poly q t)
Eq (Poly q t) =>
(Int -> Poly q t -> Int)
-> (Poly q t -> Int) -> Hashable (Poly q t)
Int -> Poly q t -> Int
Poly q t -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall (q :: ImplicitQuantification) t. Hashable t => Eq (Poly q t)
forall (q :: ImplicitQuantification) t.
Hashable t =>
Int -> Poly q t -> Int
forall (q :: ImplicitQuantification) t.
Hashable t =>
Poly q t -> Int
$chashWithSalt :: forall (q :: ImplicitQuantification) t.
Hashable t =>
Int -> Poly q t -> Int
hashWithSalt :: Int -> Poly q t -> Int
$chash :: forall (q :: ImplicitQuantification) t.
Hashable t =>
Poly q t -> Int
hash :: Poly q t -> Int
Hashable)

-- | Create a raw, unquantified @Poly@ value.
mkPoly :: [Var] -> t -> Poly 'Unquantified t
mkPoly :: forall t. [Text] -> t -> Poly 'Unquantified t
mkPoly = [Text] -> t -> Poly 'Unquantified t
forall (q :: ImplicitQuantification) t. [Text] -> t -> Poly q t
Forall

-- | Create a polytype while performing implicit quantification.
mkQPoly :: Typical t => t -> Poly 'Quantified t
mkQPoly :: forall t. Typical t => t -> Poly 'Quantified t
mkQPoly = Poly 'Unquantified t -> Poly 'Quantified t
forall t. Typical t => Poly 'Unquantified t -> Poly 'Quantified t
absQuantify (Poly 'Unquantified t -> Poly 'Quantified t)
-> (t -> Poly 'Unquantified t) -> t -> Poly 'Quantified t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> t -> Poly 'Unquantified t
forall (q :: ImplicitQuantification) t. [Text] -> t -> Poly q t
Forall []

-- | Create a trivial "polytype" with no bound variables.  This is
--   somewhat unsafe --- only use this if you are sure that the polytype
--   you want has no type variables.
mkTrivPoly :: t -> Poly q t
mkTrivPoly :: forall t (q :: ImplicitQuantification). t -> Poly q t
mkTrivPoly = [Text] -> t -> Poly q t
forall (q :: ImplicitQuantification) t. [Text] -> t -> Poly q t
Forall []

-- | Project out the variables and body of a 'Poly' value.  It's only
--   possible to project from a 'Poly Quantified' since the list of
--   variables might be meaningless for a type that has not had
--   implicit quantification applied.
unPoly :: Poly 'Quantified t -> ([Var], t)
unPoly :: forall t. Poly 'Quantified t -> ([Text], t)
unPoly (Forall [Text]
xs t
t) = ([Text]
xs, t
t)

-- | Project out the variables of a 'Poly Quantified' value.
ptVars :: Poly 'Quantified t -> [Var]
ptVars :: forall t. Poly 'Quantified t -> [Text]
ptVars (Forall [Text]
xs t
_) = [Text]
xs

-- | Forget that a polytype has been properly quantified.
forgetQ :: Poly 'Quantified t -> Poly 'Unquantified t
forgetQ :: forall t. Poly 'Quantified t -> Poly 'Unquantified t
forgetQ (Forall [Text]
xs t
t) = [Text] -> t -> Poly 'Unquantified t
forall (q :: ImplicitQuantification) t. [Text] -> t -> Poly q t
Forall [Text]
xs t
t

-- | A regular polytype (without unification variables).  A @Polytype@
--   (as opposed to a @RawPolytype@) is guaranteed to have implicit
--   quantification properly applied, so that all type variables bound
--   by the forall are explicitly listed.
type Polytype = Poly 'Quantified Type

-- | A raw polytype (without unification variables), which corresponds
--   exactly to the way a polytype was written in source code.  In
--   particular there may be type variables which are used in the type
--   but not listed explicitly, which are to be implicitly quantified.
type RawPolytype = Poly 'Unquantified Type

instance PrettyPrec (Poly q Type) where
  prettyPrec :: forall ann. Int -> Poly q Type -> Doc ann
prettyPrec Int
_ (Forall [] Type
t) = Type -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Type
t
  prettyPrec Int
_ (Forall [Text]
xs Type
t) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep (Doc ann
"∀" Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (Text -> Doc ann) -> [Text] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr [Text]
xs) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"." Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Type
t

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

instance PrettyPrec (Poly q UType) where
  prettyPrec :: forall ann. Int -> Poly q UType -> Doc ann
prettyPrec Int
_ (Forall [] UType
t) = UType -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr UType
t
  prettyPrec Int
_ (Forall [Text]
xs UType
t) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep (Doc ann
"∀" Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (Text -> Doc ann) -> [Text] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr [Text]
xs) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"." Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> UType -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr UType
t

------------------------------------------------------------
-- 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 x <- Fix (TyVarF _ x)
  where
    TyVar Text
x = TypeF Type -> Type
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Text -> Text -> TypeF Type
forall t. Text -> Text -> TypeF t
TyVarF Text
x Text
x)

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

pattern TyType :: Type
pattern $mTyType :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
$bTyType :: Type
TyType = TyBase BType

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 :: TDVar -> [Type] -> Type
pattern $mTyUser :: forall {r}. Type -> (TDVar -> [Type] -> r) -> ((# #) -> r) -> r
$bTyUser :: TDVar -> [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 x <- Free (TyVarF _ x)
  where
    UTyVar Text
x = TypeF UType -> UType
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free (Text -> Text -> TypeF UType
forall t. Text -> Text -> TypeF t
TyVarF Text
x Text
x)

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

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 UTyType :: UType
pattern $mUTyType :: forall {r}. UType -> ((# #) -> r) -> ((# #) -> r) -> r
$bUTyType :: UType
UTyType = UTyBase BType

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 :: TDVar -> [UType] -> UType
pattern $mUTyUser :: forall {r}. UType -> (TDVar -> [UType] -> r) -> ((# #) -> r) -> r
$bUTyUser :: TDVar -> [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 Var 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 Var UPolytype

-- | A @TVCtx@ tracks which type variables are in scope, and what
--   skolem variables were assigned to them.
type TVCtx = Ctx Var UType

------------------------------------------------------------
-- Implicit quantification of polytypes
------------------------------------------------------------

-- | Implicitly quantify any otherwise unbound type variables.
quantify ::
  (Has (Reader TVCtx) sig m, Typical ty) =>
  Poly 'Unquantified ty ->
  m (Poly 'Quantified ty)
quantify :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty.
(Has (Reader TVCtx) sig m, Typical ty) =>
Poly 'Unquantified ty -> m (Poly 'Quantified ty)
quantify (Forall [Text]
xs ty
ty) = do
  TVCtx
inScope <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @TVCtx
  -- Look at all variables which occur in the type but are not
  -- explicitly bound by the forall, and and are not bound in the
  -- context.  Such variables must be implicitly quantified.
  let implicit :: Set Text
implicit =
        (ty -> Set Text
forall t. Typical t => t -> Set Text
tyVars ty
ty Set Text -> Set Text -> Set Text
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` [Text] -> Set Text
forall a. Ord a => [a] -> Set a
S.fromList [Text]
xs)
          Set Text -> Set Text -> Set Text
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Map Text UType -> Set Text
forall k a. Map k a -> Set k
M.keysSet (TVCtx -> Map Text UType
forall v t. Ctx v t -> Map v t
Ctx.unCtx TVCtx
inScope)
  Poly 'Quantified ty -> m (Poly 'Quantified ty)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Poly 'Quantified ty -> m (Poly 'Quantified ty))
-> Poly 'Quantified ty -> m (Poly 'Quantified ty)
forall a b. (a -> b) -> a -> b
$ [Text] -> ty -> Poly 'Quantified ty
forall (q :: ImplicitQuantification) t. [Text] -> t -> Poly q t
Forall ([Text]
xs [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ Set Text -> [Text]
forall a. Set a -> [a]
S.toList Set Text
implicit) ty
ty

-- | Absolute implicit quantification, i.e. assume there are no type
--   variables in scope.
absQuantify :: Typical t => Poly 'Unquantified t -> Poly 'Quantified t
absQuantify :: forall t. Typical t => Poly 'Unquantified t -> Poly 'Quantified t
absQuantify = Identity (Poly 'Quantified t) -> Poly 'Quantified t
forall a. Identity a -> a
run (Identity (Poly 'Quantified t) -> Poly 'Quantified t)
-> (Poly 'Unquantified t -> Identity (Poly 'Quantified t))
-> Poly 'Unquantified t
-> Poly 'Quantified t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r (m :: * -> *) a. r -> ReaderC r m a -> m a
runReader @TVCtx TVCtx
forall v t. Ctx v t
Ctx.empty (ReaderC TVCtx Identity (Poly 'Quantified t)
 -> Identity (Poly 'Quantified t))
-> (Poly 'Unquantified t
    -> ReaderC TVCtx Identity (Poly 'Quantified t))
-> Poly 'Unquantified t
-> Identity (Poly 'Quantified t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly 'Unquantified t -> ReaderC TVCtx Identity (Poly 'Quantified t)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty.
(Has (Reader TVCtx) sig m, Typical ty) =>
Poly 'Unquantified ty -> m (Poly 'Quantified ty)
quantify

------------------------------------------------------------
-- 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, Eq TydefInfo
Eq TydefInfo =>
(Int -> TydefInfo -> Int)
-> (TydefInfo -> Int) -> Hashable TydefInfo
Int -> TydefInfo -> Int
TydefInfo -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> TydefInfo -> Int
hashWithSalt :: Int -> TydefInfo -> Int
$chash :: TydefInfo -> Int
hash :: TydefInfo -> Int
Hashable)

makeLenses ''TydefInfo

-- | A @TDCtx@ is a mapping from user-defined type constructor names
--   to their definitions and arities/kinds.  It also stores the
--   latest version of each name (for any names with more than one
--   version), so we can tell when a type definition has been
--   shadowed.
data TDCtx = TDCtx
  { TDCtx -> Ctx TDVar TydefInfo
getTDCtx :: Ctx TDVar TydefInfo
  , TDCtx -> MonoidMap Text (Sum Int)
getTDVersions :: MonoidMap Text (Sum Int)
  }
  deriving (TDCtx -> TDCtx -> Bool
(TDCtx -> TDCtx -> Bool) -> (TDCtx -> TDCtx -> Bool) -> Eq TDCtx
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TDCtx -> TDCtx -> Bool
== :: TDCtx -> TDCtx -> Bool
$c/= :: TDCtx -> TDCtx -> Bool
/= :: TDCtx -> TDCtx -> Bool
Eq, (forall x. TDCtx -> Rep TDCtx x)
-> (forall x. Rep TDCtx x -> TDCtx) -> Generic TDCtx
forall x. Rep TDCtx x -> TDCtx
forall x. TDCtx -> Rep TDCtx x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TDCtx -> Rep TDCtx x
from :: forall x. TDCtx -> Rep TDCtx x
$cto :: forall x. Rep TDCtx x -> TDCtx
to :: forall x. Rep TDCtx x -> TDCtx
Generic, Int -> TDCtx -> ShowS
[TDCtx] -> ShowS
TDCtx -> [Char]
(Int -> TDCtx -> ShowS)
-> (TDCtx -> [Char]) -> ([TDCtx] -> ShowS) -> Show TDCtx
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TDCtx -> ShowS
showsPrec :: Int -> TDCtx -> ShowS
$cshow :: TDCtx -> [Char]
show :: TDCtx -> [Char]
$cshowList :: [TDCtx] -> ShowS
showList :: [TDCtx] -> ShowS
Show, [TDCtx] -> Value
[TDCtx] -> Encoding
TDCtx -> Bool
TDCtx -> Value
TDCtx -> Encoding
(TDCtx -> Value)
-> (TDCtx -> Encoding)
-> ([TDCtx] -> Value)
-> ([TDCtx] -> Encoding)
-> (TDCtx -> Bool)
-> ToJSON TDCtx
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: TDCtx -> Value
toJSON :: TDCtx -> Value
$ctoEncoding :: TDCtx -> Encoding
toEncoding :: TDCtx -> Encoding
$ctoJSONList :: [TDCtx] -> Value
toJSONList :: [TDCtx] -> Value
$ctoEncodingList :: [TDCtx] -> Encoding
toEncodingList :: [TDCtx] -> Encoding
$comitField :: TDCtx -> Bool
omitField :: TDCtx -> Bool
ToJSON)

-- Need to write manual Hashable instance since MonoidMap
-- does not have instances of its own.

instance Hashable TDCtx where
  hashWithSalt :: Int -> TDCtx -> Int
hashWithSalt Int
s (TDCtx Ctx TDVar TydefInfo
ctx MonoidMap Text (Sum Int)
versions) =
    Int
s
      Int -> Ctx TDVar TydefInfo -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Ctx TDVar TydefInfo
ctx
      Int -> Map Text Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Sum Int -> Int
forall a. Sum a -> a
getSum (Sum Int -> Int) -> Map Text (Sum Int) -> Map Text Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MonoidMap Text (Sum Int) -> Map Text (Sum Int)
forall k v. MonoidMap k v -> Map k v
MM.toMap MonoidMap Text (Sum Int)
versions)

-- | The empty type definition context.
emptyTDCtx :: TDCtx
emptyTDCtx :: TDCtx
emptyTDCtx = Ctx TDVar TydefInfo -> MonoidMap Text (Sum Int) -> TDCtx
TDCtx Ctx TDVar TydefInfo
forall v t. Ctx v t
Ctx.empty MonoidMap Text (Sum Int)
forall k v. MonoidMap k v
MM.empty

-- | Look up a variable in the type definition context.
lookupTD :: TDVar -> TDCtx -> Maybe TydefInfo
lookupTD :: TDVar -> TDCtx -> Maybe TydefInfo
lookupTD TDVar
x = TDVar -> Ctx TDVar TydefInfo -> Maybe TydefInfo
forall v t. Ord v => v -> Ctx v t -> Maybe t
Ctx.lookup TDVar
x (Ctx TDVar TydefInfo -> Maybe TydefInfo)
-> (TDCtx -> Ctx TDVar TydefInfo) -> TDCtx -> Maybe TydefInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TDCtx -> Ctx TDVar TydefInfo
getTDCtx

-- | Look up a variable in an ambient type definition context.
lookupTDR :: Has (Reader TDCtx) sig m => TDVar -> m (Maybe TydefInfo)
lookupTDR :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader TDCtx) sig m =>
TDVar -> m (Maybe TydefInfo)
lookupTDR TDVar
x = TDVar -> TDCtx -> Maybe TydefInfo
lookupTD TDVar
x (TDCtx -> Maybe TydefInfo) -> m TDCtx -> m (Maybe TydefInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m TDCtx
forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask

-- | Add a binding of a variable name to a type definition, giving it
--   an appropriate version number if it shadows other variables with
--   the same name.
addBindingTD :: Text -> TydefInfo -> TDCtx -> TDCtx
addBindingTD :: Text -> TydefInfo -> TDCtx -> TDCtx
addBindingTD Text
x TydefInfo
info (TDCtx Ctx TDVar TydefInfo
tdCtx MonoidMap Text (Sum Int)
tdVersions) =
  case TDVar -> Ctx TDVar TydefInfo -> Maybe TydefInfo
forall v t. Ord v => v -> Ctx v t -> Maybe t
Ctx.lookup (Text -> TDVar
mkTDVar Text
x) Ctx TDVar TydefInfo
tdCtx of
    Maybe TydefInfo
Nothing -> Ctx TDVar TydefInfo -> MonoidMap Text (Sum Int) -> TDCtx
TDCtx (TDVar -> TydefInfo -> Ctx TDVar TydefInfo -> Ctx TDVar TydefInfo
forall v t.
(Ord v, Hashable v, Hashable t) =>
v -> t -> Ctx v t -> Ctx v t
Ctx.addBinding (Text -> TDVar
mkTDVar Text
x) TydefInfo
info Ctx TDVar TydefInfo
tdCtx) MonoidMap Text (Sum Int)
tdVersions
    Just TydefInfo
_ ->
      let newVersion :: Sum Int
newVersion = Sum Int
1 Sum Int -> Sum Int -> Sum Int
forall a. Num a => a -> a -> a
+ Text -> MonoidMap Text (Sum Int) -> Sum Int
forall k v. (Ord k, Monoid v) => k -> MonoidMap k v -> v
MM.get Text
x MonoidMap Text (Sum Int)
tdVersions
       in Ctx TDVar TydefInfo -> MonoidMap Text (Sum Int) -> TDCtx
TDCtx (TDVar -> TydefInfo -> Ctx TDVar TydefInfo -> Ctx TDVar TydefInfo
forall v t.
(Ord v, Hashable v, Hashable t) =>
v -> t -> Ctx v t -> Ctx v t
Ctx.addBinding (Int -> Text -> TDVar
mkTDVar' (Sum Int -> Int
forall a. Sum a -> a
getSum Sum Int
newVersion) Text
x) TydefInfo
info Ctx TDVar TydefInfo
tdCtx) (Text
-> Sum Int -> MonoidMap Text (Sum Int) -> MonoidMap Text (Sum Int)
forall k v.
(Ord k, MonoidNull v) =>
k -> v -> MonoidMap k v -> MonoidMap k v
MM.set Text
x Sum Int
newVersion MonoidMap Text (Sum Int)
tdVersions)

-- | Locally extend the ambient type definition context with an
--   additional binding, via 'addBindingTD'.
withBindingTD :: Has (Reader TDCtx) sig m => Text -> TydefInfo -> m a -> m a
withBindingTD :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader TDCtx) sig m =>
Text -> TydefInfo -> m a -> m a
withBindingTD Text
x TydefInfo
info = (TDCtx -> TDCtx) -> m a -> m a
forall r (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader r) sig m =>
(r -> r) -> m a -> m a
local (Text -> TydefInfo -> TDCtx -> TDCtx
addBindingTD Text
x TydefInfo
info)

-- | Given a parsed variable representing a user-defined type, figure
--   out which version is currently in scope and set the version
--   number of the variable appropriately.
resolveUserTy :: Has (Reader TDCtx) sig m => TDVar -> m TDVar
resolveUserTy :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader TDCtx) sig m =>
TDVar -> m TDVar
resolveUserTy TDVar
v = do
  TDCtx
tdCtx <- m TDCtx
forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask
  let x :: Text
x = TDVar -> Text
tdVarName TDVar
v
  let ver :: Int
ver = Sum Int -> Int
forall a. Sum a -> a
getSum (Text -> MonoidMap Text (Sum Int) -> Sum Int
forall k v. (Ord k, Monoid v) => k -> MonoidMap k v -> v
MM.get Text
x (TDCtx -> MonoidMap Text (Sum Int)
getTDVersions TDCtx
tdCtx))
  TDVar -> m TDVar
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TDVar -> m TDVar) -> TDVar -> m TDVar
forall a b. (a -> b) -> a -> b
$ Int -> Text -> TDVar
mkTDVar' Int
ver Text
x

newtype ExpandTydefErr = UnexpandedUserType {ExpandTydefErr -> TDVar
getUnexpanded :: TDVar}
  deriving (ExpandTydefErr -> ExpandTydefErr -> Bool
(ExpandTydefErr -> ExpandTydefErr -> Bool)
-> (ExpandTydefErr -> ExpandTydefErr -> Bool) -> Eq ExpandTydefErr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ExpandTydefErr -> ExpandTydefErr -> Bool
== :: ExpandTydefErr -> ExpandTydefErr -> Bool
$c/= :: ExpandTydefErr -> ExpandTydefErr -> Bool
/= :: ExpandTydefErr -> ExpandTydefErr -> Bool
Eq, Int -> ExpandTydefErr -> ShowS
[ExpandTydefErr] -> ShowS
ExpandTydefErr -> [Char]
(Int -> ExpandTydefErr -> ShowS)
-> (ExpandTydefErr -> [Char])
-> ([ExpandTydefErr] -> ShowS)
-> Show ExpandTydefErr
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExpandTydefErr -> ShowS
showsPrec :: Int -> ExpandTydefErr -> ShowS
$cshow :: ExpandTydefErr -> [Char]
show :: ExpandTydefErr -> [Char]
$cshowList :: [ExpandTydefErr] -> ShowS
showList :: [ExpandTydefErr] -> ShowS
Show)

-- | 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, and user types must be
--   defined; we don't worry about what happens if the lists have
--   different lengths since in theory that can never happen.
--   However, if T does not exist, we throw an error containing its
--   name.
expandTydef ::
  ( Has (Reader TDCtx) sig m
  , Has (Throw ExpandTydefErr) sig m
  , Typical t
  ) =>
  TDVar ->
  [t] ->
  m t
expandTydef :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) t.
(Has (Reader TDCtx) sig m, Has (Throw ExpandTydefErr) sig m,
 Typical t) =>
TDVar -> [t] -> m t
expandTydef TDVar
userTyCon [t]
tys = do
  Maybe TydefInfo
mtydefInfo <- TDVar -> m (Maybe TydefInfo)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader TDCtx) sig m =>
TDVar -> m (Maybe TydefInfo)
lookupTDR TDVar
userTyCon
  case Maybe TydefInfo
mtydefInfo of
    Maybe TydefInfo
Nothing -> ExpandTydefErr -> m t
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (TDVar -> ExpandTydefErr
UnexpandedUserType TDVar
userTyCon)
    Just TydefInfo
tydefInfo -> t -> m t
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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

-- | Expand *all* applications of user-defined type constructors
--   everywhere in a type.
expandTydefs ::
  (Has (Reader TDCtx) sig m, Has (Throw ExpandTydefErr) sig m, Typical t, Plated t) =>
  t ->
  m t
expandTydefs :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) t.
(Has (Reader TDCtx) sig m, Has (Throw ExpandTydefErr) sig m,
 Typical t, Plated t) =>
t -> m t
expandTydefs = (t -> m (Maybe t)) -> t -> m t
forall (m :: * -> *) a.
(Monad m, Plated a) =>
(a -> m (Maybe a)) -> a -> m a
rewriteM t -> m (Maybe t)
forall {a} {f :: * -> *} {sig :: (* -> *) -> * -> *}.
(Typical a, Algebra sig f, Member (Reader TDCtx) sig,
 Member (Throw ExpandTydefErr) sig) =>
a -> f (Maybe a)
expand
 where
  -- expand :: t -> m (Maybe t)
  expand :: a -> f (Maybe a)
expand a
t = case a -> Maybe (TypeF a)
forall t. Typical t => t -> Maybe (TypeF t)
unrollT a
t of
    Just (TyConF (TCUser TDVar
u) [a]
tys) -> a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> f a -> f (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TDVar -> [a] -> f a
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) t.
(Has (Reader TDCtx) sig m, Has (Throw ExpandTydefErr) sig m,
 Typical t) =>
TDVar -> [t] -> m t
expandTydef TDVar
u [a]
tys
    Maybe (TypeF a)
_ -> Maybe a -> f (Maybe a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing

-- | 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
refoldT @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
_ 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 => TDVar -> TydefInfo -> t -> t
elimTydef :: forall t. Typical t => TDVar -> TydefInfo -> t -> t
elimTydef TDVar
x TydefInfo
tdInfo = (TypeF t -> t) -> t -> t
forall t. Typical t => (TypeF t -> t) -> t -> t
refoldT TypeF t -> t
substF
 where
  substF :: TypeF t -> t
substF = \case
    TyConF (TCUser TDVar
u) [t]
tys | TDVar
u TDVar -> TDVar -> Bool
forall a. Eq a => a -> a -> Bool
== TDVar
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 TDVar
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
<$> TDVar -> TDCtx -> Maybe TydefInfo
lookupTD TDVar
t TDCtx
tydefs

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

-- | Reduce a type to weak head normal form, i.e. keep unfolding type
--   aliases and recursive types just until the top-level constructor
--   of the type is neither @rec@ nor an application of a defined 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 TDVar
u [Type]
tys -> do
      Either ExpandTydefErr Type
res <- forall e (m :: * -> *) a. ThrowC e m a -> m (Either e a)
runThrow @ExpandTydefErr (TDVar -> [Type] -> ThrowC ExpandTydefErr m Type
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) t.
(Has (Reader TDCtx) sig m, Has (Throw ExpandTydefErr) sig m,
 Typical t) =>
TDVar -> [t] -> m t
expandTydef TDVar
u [Type]
tys)
      case Either ExpandTydefErr Type
res of
        Left ExpandTydefErr
_ -> Type -> m Type
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ TDVar -> [Type] -> Type
TyUser TDVar
u [Type]
tys
        Right Type
expTy -> Type -> m Type
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader TDCtx) sig m =>
Type -> m Type
go Type
expTy
    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