-- |
-- Data types for types
--
module Language.PureScript.Types where

import Prelude.Compat
import Protolude (ordNub)

import Codec.Serialise (Serialise)
import Control.Applicative ((<|>))
import Control.Arrow (first, second)
import Control.DeepSeq (NFData)
import Control.Monad ((<=<), (>=>))
import Data.Aeson ((.:), (.:?), (.!=), (.=))
import qualified Data.Aeson as A
import qualified Data.Aeson.Types as A
import Data.Foldable (fold)
import qualified Data.IntSet as IS
import Data.List (sort, sortBy)
import Data.Ord (comparing)
import Data.Maybe (fromMaybe, isJust)
import qualified Data.Set as S
import Data.Text (Text)
import qualified Data.Text as T
import GHC.Generics (Generic)

import Language.PureScript.AST.SourcePos
import qualified Language.PureScript.Constants.Prim as C
import Language.PureScript.Names
import Language.PureScript.Label (Label)
import Language.PureScript.PSString (PSString)

import Lens.Micro (Lens', (^.), set)

type SourceType = Type SourceAnn
type SourceConstraint = Constraint SourceAnn

-- |
-- An identifier for the scope of a skolem variable
--
newtype SkolemScope = SkolemScope { SkolemScope -> Int
runSkolemScope :: Int }
  deriving (Int -> SkolemScope -> ShowS
[SkolemScope] -> ShowS
SkolemScope -> String
(Int -> SkolemScope -> ShowS)
-> (SkolemScope -> String)
-> ([SkolemScope] -> ShowS)
-> Show SkolemScope
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SkolemScope] -> ShowS
$cshowList :: [SkolemScope] -> ShowS
show :: SkolemScope -> String
$cshow :: SkolemScope -> String
showsPrec :: Int -> SkolemScope -> ShowS
$cshowsPrec :: Int -> SkolemScope -> ShowS
Show, SkolemScope -> SkolemScope -> Bool
(SkolemScope -> SkolemScope -> Bool)
-> (SkolemScope -> SkolemScope -> Bool) -> Eq SkolemScope
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SkolemScope -> SkolemScope -> Bool
$c/= :: SkolemScope -> SkolemScope -> Bool
== :: SkolemScope -> SkolemScope -> Bool
$c== :: SkolemScope -> SkolemScope -> Bool
Eq, Eq SkolemScope
Eq SkolemScope
-> (SkolemScope -> SkolemScope -> Ordering)
-> (SkolemScope -> SkolemScope -> Bool)
-> (SkolemScope -> SkolemScope -> Bool)
-> (SkolemScope -> SkolemScope -> Bool)
-> (SkolemScope -> SkolemScope -> Bool)
-> (SkolemScope -> SkolemScope -> SkolemScope)
-> (SkolemScope -> SkolemScope -> SkolemScope)
-> Ord SkolemScope
SkolemScope -> SkolemScope -> Bool
SkolemScope -> SkolemScope -> Ordering
SkolemScope -> SkolemScope -> SkolemScope
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SkolemScope -> SkolemScope -> SkolemScope
$cmin :: SkolemScope -> SkolemScope -> SkolemScope
max :: SkolemScope -> SkolemScope -> SkolemScope
$cmax :: SkolemScope -> SkolemScope -> SkolemScope
>= :: SkolemScope -> SkolemScope -> Bool
$c>= :: SkolemScope -> SkolemScope -> Bool
> :: SkolemScope -> SkolemScope -> Bool
$c> :: SkolemScope -> SkolemScope -> Bool
<= :: SkolemScope -> SkolemScope -> Bool
$c<= :: SkolemScope -> SkolemScope -> Bool
< :: SkolemScope -> SkolemScope -> Bool
$c< :: SkolemScope -> SkolemScope -> Bool
compare :: SkolemScope -> SkolemScope -> Ordering
$ccompare :: SkolemScope -> SkolemScope -> Ordering
$cp1Ord :: Eq SkolemScope
Ord, [SkolemScope] -> Encoding
[SkolemScope] -> Value
SkolemScope -> Encoding
SkolemScope -> Value
(SkolemScope -> Value)
-> (SkolemScope -> Encoding)
-> ([SkolemScope] -> Value)
-> ([SkolemScope] -> Encoding)
-> ToJSON SkolemScope
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [SkolemScope] -> Encoding
$ctoEncodingList :: [SkolemScope] -> Encoding
toJSONList :: [SkolemScope] -> Value
$ctoJSONList :: [SkolemScope] -> Value
toEncoding :: SkolemScope -> Encoding
$ctoEncoding :: SkolemScope -> Encoding
toJSON :: SkolemScope -> Value
$ctoJSON :: SkolemScope -> Value
A.ToJSON, Value -> Parser [SkolemScope]
Value -> Parser SkolemScope
(Value -> Parser SkolemScope)
-> (Value -> Parser [SkolemScope]) -> FromJSON SkolemScope
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [SkolemScope]
$cparseJSONList :: Value -> Parser [SkolemScope]
parseJSON :: Value -> Parser SkolemScope
$cparseJSON :: Value -> Parser SkolemScope
A.FromJSON, (forall x. SkolemScope -> Rep SkolemScope x)
-> (forall x. Rep SkolemScope x -> SkolemScope)
-> Generic SkolemScope
forall x. Rep SkolemScope x -> SkolemScope
forall x. SkolemScope -> Rep SkolemScope x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SkolemScope x -> SkolemScope
$cfrom :: forall x. SkolemScope -> Rep SkolemScope x
Generic)

instance NFData SkolemScope
instance Serialise SkolemScope

-- |
-- The type of types
--
data Type a
  -- | A unification variable of type Type
  = TUnknown a Int
  -- | A named type variable
  | TypeVar a Text
  -- | A type-level string
  | TypeLevelString a PSString
  -- | A type wildcard, as would appear in a partial type synonym
  | TypeWildcard a (Maybe Text)
  -- | A type constructor
  | TypeConstructor a (Qualified (ProperName 'TypeName))
  -- | A type operator. This will be desugared into a type constructor during the
  -- "operators" phase of desugaring.
  | TypeOp a (Qualified (OpName 'TypeOpName))
  -- | A type application
  | TypeApp a (Type a) (Type a)
  -- | Explicit kind application
  | KindApp a (Type a) (Type a)
  -- | Forall quantifier
  | ForAll a Text (Maybe (Type a)) (Type a) (Maybe SkolemScope)
  -- | A type with a set of type class constraints
  | ConstrainedType a (Constraint a) (Type a)
  -- | A skolem constant
  | Skolem a Text (Maybe (Type a)) Int SkolemScope
  -- | An empty row
  | REmpty a
  -- | A non-empty row
  | RCons a Label (Type a) (Type a)
  -- | A type with a kind annotation
  | KindedType a (Type a) (Type a)
  -- | Binary operator application. During the rebracketing phase of desugaring,
  -- this data constructor will be removed.
  | BinaryNoParensType a (Type a) (Type a) (Type a)
  -- | Explicit parentheses. During the rebracketing phase of desugaring, this
  -- data constructor will be removed.
  --
  -- Note: although it seems this constructor is not used, it _is_ useful,
  -- since it prevents certain traversals from matching.
  | ParensInType a (Type a)
  deriving (Int -> Type a -> ShowS
[Type a] -> ShowS
Type a -> String
(Int -> Type a -> ShowS)
-> (Type a -> String) -> ([Type a] -> ShowS) -> Show (Type a)
forall a. Show a => Int -> Type a -> ShowS
forall a. Show a => [Type a] -> ShowS
forall a. Show a => Type a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Type a] -> ShowS
$cshowList :: forall a. Show a => [Type a] -> ShowS
show :: Type a -> String
$cshow :: forall a. Show a => Type a -> String
showsPrec :: Int -> Type a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Type a -> ShowS
Show, (forall x. Type a -> Rep (Type a) x)
-> (forall x. Rep (Type a) x -> Type a) -> Generic (Type a)
forall x. Rep (Type a) x -> Type a
forall x. Type a -> Rep (Type a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Type a) x -> Type a
forall a x. Type a -> Rep (Type a) x
$cto :: forall a x. Rep (Type a) x -> Type a
$cfrom :: forall a x. Type a -> Rep (Type a) x
Generic, a -> Type b -> Type a
(a -> b) -> Type a -> Type b
(forall a b. (a -> b) -> Type a -> Type b)
-> (forall a b. a -> Type b -> Type a) -> Functor Type
forall a b. a -> Type b -> Type a
forall a b. (a -> b) -> Type a -> Type b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Type b -> Type a
$c<$ :: forall a b. a -> Type b -> Type a
fmap :: (a -> b) -> Type a -> Type b
$cfmap :: forall a b. (a -> b) -> Type a -> Type b
Functor, Type a -> Bool
(a -> m) -> Type a -> m
(a -> b -> b) -> b -> Type a -> b
(forall m. Monoid m => Type m -> m)
-> (forall m a. Monoid m => (a -> m) -> Type a -> m)
-> (forall m a. Monoid m => (a -> m) -> Type a -> m)
-> (forall a b. (a -> b -> b) -> b -> Type a -> b)
-> (forall a b. (a -> b -> b) -> b -> Type a -> b)
-> (forall b a. (b -> a -> b) -> b -> Type a -> b)
-> (forall b a. (b -> a -> b) -> b -> Type a -> b)
-> (forall a. (a -> a -> a) -> Type a -> a)
-> (forall a. (a -> a -> a) -> Type a -> a)
-> (forall a. Type a -> [a])
-> (forall a. Type a -> Bool)
-> (forall a. Type a -> Int)
-> (forall a. Eq a => a -> Type a -> Bool)
-> (forall a. Ord a => Type a -> a)
-> (forall a. Ord a => Type a -> a)
-> (forall a. Num a => Type a -> a)
-> (forall a. Num a => Type a -> a)
-> Foldable Type
forall a. Eq a => a -> Type a -> Bool
forall a. Num a => Type a -> a
forall a. Ord a => Type a -> a
forall m. Monoid m => Type m -> m
forall a. Type a -> Bool
forall a. Type a -> Int
forall a. Type a -> [a]
forall a. (a -> a -> a) -> Type a -> a
forall m a. Monoid m => (a -> m) -> Type a -> m
forall b a. (b -> a -> b) -> b -> Type a -> b
forall a b. (a -> b -> b) -> b -> Type a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Type a -> a
$cproduct :: forall a. Num a => Type a -> a
sum :: Type a -> a
$csum :: forall a. Num a => Type a -> a
minimum :: Type a -> a
$cminimum :: forall a. Ord a => Type a -> a
maximum :: Type a -> a
$cmaximum :: forall a. Ord a => Type a -> a
elem :: a -> Type a -> Bool
$celem :: forall a. Eq a => a -> Type a -> Bool
length :: Type a -> Int
$clength :: forall a. Type a -> Int
null :: Type a -> Bool
$cnull :: forall a. Type a -> Bool
toList :: Type a -> [a]
$ctoList :: forall a. Type a -> [a]
foldl1 :: (a -> a -> a) -> Type a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Type a -> a
foldr1 :: (a -> a -> a) -> Type a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Type a -> a
foldl' :: (b -> a -> b) -> b -> Type a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Type a -> b
foldl :: (b -> a -> b) -> b -> Type a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Type a -> b
foldr' :: (a -> b -> b) -> b -> Type a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Type a -> b
foldr :: (a -> b -> b) -> b -> Type a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Type a -> b
foldMap' :: (a -> m) -> Type a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Type a -> m
foldMap :: (a -> m) -> Type a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Type a -> m
fold :: Type m -> m
$cfold :: forall m. Monoid m => Type m -> m
Foldable, Functor Type
Foldable Type
Functor Type
-> Foldable Type
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Type a -> f (Type b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Type (f a) -> f (Type a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Type a -> m (Type b))
-> (forall (m :: * -> *) a. Monad m => Type (m a) -> m (Type a))
-> Traversable Type
(a -> f b) -> Type a -> f (Type 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 => Type (m a) -> m (Type a)
forall (f :: * -> *) a. Applicative f => Type (f a) -> f (Type a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type a -> m (Type b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type a -> f (Type b)
sequence :: Type (m a) -> m (Type a)
$csequence :: forall (m :: * -> *) a. Monad m => Type (m a) -> m (Type a)
mapM :: (a -> m b) -> Type a -> m (Type b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type a -> m (Type b)
sequenceA :: Type (f a) -> f (Type a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Type (f a) -> f (Type a)
traverse :: (a -> f b) -> Type a -> f (Type b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type a -> f (Type b)
$cp2Traversable :: Foldable Type
$cp1Traversable :: Functor Type
Traversable)

instance NFData a => NFData (Type a)
instance Serialise a => Serialise (Type a)

srcTUnknown :: Int -> SourceType
srcTUnknown :: Int -> SourceType
srcTUnknown = SourceAnn -> Int -> SourceType
forall a. a -> Int -> Type a
TUnknown SourceAnn
NullSourceAnn

srcTypeVar :: Text -> SourceType
srcTypeVar :: Text -> SourceType
srcTypeVar = SourceAnn -> Text -> SourceType
forall a. a -> Text -> Type a
TypeVar SourceAnn
NullSourceAnn

srcTypeLevelString :: PSString -> SourceType
srcTypeLevelString :: PSString -> SourceType
srcTypeLevelString = SourceAnn -> PSString -> SourceType
forall a. a -> PSString -> Type a
TypeLevelString SourceAnn
NullSourceAnn

srcTypeWildcard :: SourceType
srcTypeWildcard :: SourceType
srcTypeWildcard = SourceAnn -> Maybe Text -> SourceType
forall a. a -> Maybe Text -> Type a
TypeWildcard SourceAnn
NullSourceAnn Maybe Text
forall a. Maybe a
Nothing

srcTypeConstructor :: Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor :: Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor = SourceAnn -> Qualified (ProperName 'TypeName) -> SourceType
forall a. a -> Qualified (ProperName 'TypeName) -> Type a
TypeConstructor SourceAnn
NullSourceAnn

srcTypeOp :: Qualified (OpName 'TypeOpName) -> SourceType
srcTypeOp :: Qualified (OpName 'TypeOpName) -> SourceType
srcTypeOp = SourceAnn -> Qualified (OpName 'TypeOpName) -> SourceType
forall a. a -> Qualified (OpName 'TypeOpName) -> Type a
TypeOp SourceAnn
NullSourceAnn

srcTypeApp :: SourceType -> SourceType -> SourceType
srcTypeApp :: SourceType -> SourceType -> SourceType
srcTypeApp = SourceAnn -> SourceType -> SourceType -> SourceType
forall a. a -> Type a -> Type a -> Type a
TypeApp SourceAnn
NullSourceAnn

srcKindApp :: SourceType -> SourceType -> SourceType
srcKindApp :: SourceType -> SourceType -> SourceType
srcKindApp = SourceAnn -> SourceType -> SourceType -> SourceType
forall a. a -> Type a -> Type a -> Type a
KindApp SourceAnn
NullSourceAnn

srcForAll :: Text -> Maybe SourceType -> SourceType -> Maybe SkolemScope -> SourceType
srcForAll :: Text
-> Maybe SourceType
-> SourceType
-> Maybe SkolemScope
-> SourceType
srcForAll = SourceAnn
-> Text
-> Maybe SourceType
-> SourceType
-> Maybe SkolemScope
-> SourceType
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll SourceAnn
NullSourceAnn

srcConstrainedType :: SourceConstraint -> SourceType -> SourceType
srcConstrainedType :: SourceConstraint -> SourceType -> SourceType
srcConstrainedType = SourceAnn -> SourceConstraint -> SourceType -> SourceType
forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType SourceAnn
NullSourceAnn

srcREmpty :: SourceType
srcREmpty :: SourceType
srcREmpty = SourceAnn -> SourceType
forall a. a -> Type a
REmpty SourceAnn
NullSourceAnn

srcRCons :: Label -> SourceType -> SourceType -> SourceType
srcRCons :: Label -> SourceType -> SourceType -> SourceType
srcRCons = SourceAnn -> Label -> SourceType -> SourceType -> SourceType
forall a. a -> Label -> Type a -> Type a -> Type a
RCons SourceAnn
NullSourceAnn

srcKindedType :: SourceType -> SourceType -> SourceType
srcKindedType :: SourceType -> SourceType -> SourceType
srcKindedType = SourceAnn -> SourceType -> SourceType -> SourceType
forall a. a -> Type a -> Type a -> Type a
KindedType SourceAnn
NullSourceAnn

srcBinaryNoParensType :: SourceType -> SourceType -> SourceType -> SourceType
srcBinaryNoParensType :: SourceType -> SourceType -> SourceType -> SourceType
srcBinaryNoParensType = SourceAnn -> SourceType -> SourceType -> SourceType -> SourceType
forall a. a -> Type a -> Type a -> Type a -> Type a
BinaryNoParensType SourceAnn
NullSourceAnn

srcParensInType :: SourceType -> SourceType
srcParensInType :: SourceType -> SourceType
srcParensInType = SourceAnn -> SourceType -> SourceType
forall a. a -> Type a -> Type a
ParensInType SourceAnn
NullSourceAnn

pattern REmptyKinded :: forall a. a -> Maybe (Type a) -> Type a
pattern $mREmptyKinded :: forall r a.
Type a -> (a -> Maybe (Type a) -> r) -> (Void# -> r) -> r
REmptyKinded ann mbK <- (toREmptyKinded -> Just (ann, mbK))

toREmptyKinded :: forall a. Type a -> Maybe (a, Maybe (Type a))
toREmptyKinded :: Type a -> Maybe (a, Maybe (Type a))
toREmptyKinded (REmpty a
ann) = (a, Maybe (Type a)) -> Maybe (a, Maybe (Type a))
forall a. a -> Maybe a
Just (a
ann, Maybe (Type a)
forall a. Maybe a
Nothing)
toREmptyKinded (KindApp a
_ (REmpty a
ann) Type a
k) = (a, Maybe (Type a)) -> Maybe (a, Maybe (Type a))
forall a. a -> Maybe a
Just (a
ann, Type a -> Maybe (Type a)
forall a. a -> Maybe a
Just Type a
k)
toREmptyKinded Type a
_ = Maybe (a, Maybe (Type a))
forall a. Maybe a
Nothing

isREmpty :: forall a. Type a -> Bool
isREmpty :: Type a -> Bool
isREmpty = Maybe (a, Maybe (Type a)) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (a, Maybe (Type a)) -> Bool)
-> (Type a -> Maybe (a, Maybe (Type a))) -> Type a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type a -> Maybe (a, Maybe (Type a))
forall a. Type a -> Maybe (a, Maybe (Type a))
toREmptyKinded

-- | Additional data relevant to type class constraints
data ConstraintData
  = PartialConstraintData [[Text]] Bool
  -- ^ Data to accompany a Partial constraint generated by the exhaustivity checker.
  -- It contains (rendered) binder information for those binders which were
  -- not matched, and a flag indicating whether the list was truncated or not.
  -- Note: we use 'Text' here because using 'Binder' would introduce a cyclic
  -- dependency in the module graph.
  deriving (Int -> ConstraintData -> ShowS
[ConstraintData] -> ShowS
ConstraintData -> String
(Int -> ConstraintData -> ShowS)
-> (ConstraintData -> String)
-> ([ConstraintData] -> ShowS)
-> Show ConstraintData
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConstraintData] -> ShowS
$cshowList :: [ConstraintData] -> ShowS
show :: ConstraintData -> String
$cshow :: ConstraintData -> String
showsPrec :: Int -> ConstraintData -> ShowS
$cshowsPrec :: Int -> ConstraintData -> ShowS
Show, ConstraintData -> ConstraintData -> Bool
(ConstraintData -> ConstraintData -> Bool)
-> (ConstraintData -> ConstraintData -> Bool) -> Eq ConstraintData
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConstraintData -> ConstraintData -> Bool
$c/= :: ConstraintData -> ConstraintData -> Bool
== :: ConstraintData -> ConstraintData -> Bool
$c== :: ConstraintData -> ConstraintData -> Bool
Eq, Eq ConstraintData
Eq ConstraintData
-> (ConstraintData -> ConstraintData -> Ordering)
-> (ConstraintData -> ConstraintData -> Bool)
-> (ConstraintData -> ConstraintData -> Bool)
-> (ConstraintData -> ConstraintData -> Bool)
-> (ConstraintData -> ConstraintData -> Bool)
-> (ConstraintData -> ConstraintData -> ConstraintData)
-> (ConstraintData -> ConstraintData -> ConstraintData)
-> Ord ConstraintData
ConstraintData -> ConstraintData -> Bool
ConstraintData -> ConstraintData -> Ordering
ConstraintData -> ConstraintData -> ConstraintData
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ConstraintData -> ConstraintData -> ConstraintData
$cmin :: ConstraintData -> ConstraintData -> ConstraintData
max :: ConstraintData -> ConstraintData -> ConstraintData
$cmax :: ConstraintData -> ConstraintData -> ConstraintData
>= :: ConstraintData -> ConstraintData -> Bool
$c>= :: ConstraintData -> ConstraintData -> Bool
> :: ConstraintData -> ConstraintData -> Bool
$c> :: ConstraintData -> ConstraintData -> Bool
<= :: ConstraintData -> ConstraintData -> Bool
$c<= :: ConstraintData -> ConstraintData -> Bool
< :: ConstraintData -> ConstraintData -> Bool
$c< :: ConstraintData -> ConstraintData -> Bool
compare :: ConstraintData -> ConstraintData -> Ordering
$ccompare :: ConstraintData -> ConstraintData -> Ordering
$cp1Ord :: Eq ConstraintData
Ord, (forall x. ConstraintData -> Rep ConstraintData x)
-> (forall x. Rep ConstraintData x -> ConstraintData)
-> Generic ConstraintData
forall x. Rep ConstraintData x -> ConstraintData
forall x. ConstraintData -> Rep ConstraintData x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ConstraintData x -> ConstraintData
$cfrom :: forall x. ConstraintData -> Rep ConstraintData x
Generic)

instance NFData ConstraintData
instance Serialise ConstraintData

-- | A typeclass constraint
data Constraint a = Constraint
  { Constraint a -> a
constraintAnn :: a
  -- ^ constraint annotation
  , Constraint a -> Qualified (ProperName 'ClassName)
constraintClass :: Qualified (ProperName 'ClassName)
  -- ^ constraint class name
  , Constraint a -> [Type a]
constraintKindArgs :: [Type a]
  -- ^ kind arguments
  , Constraint a -> [Type a]
constraintArgs  :: [Type a]
  -- ^ type arguments
  , Constraint a -> Maybe ConstraintData
constraintData  :: Maybe ConstraintData
  -- ^ additional data relevant to this constraint
  } deriving (Int -> Constraint a -> ShowS
[Constraint a] -> ShowS
Constraint a -> String
(Int -> Constraint a -> ShowS)
-> (Constraint a -> String)
-> ([Constraint a] -> ShowS)
-> Show (Constraint a)
forall a. Show a => Int -> Constraint a -> ShowS
forall a. Show a => [Constraint a] -> ShowS
forall a. Show a => Constraint a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Constraint a] -> ShowS
$cshowList :: forall a. Show a => [Constraint a] -> ShowS
show :: Constraint a -> String
$cshow :: forall a. Show a => Constraint a -> String
showsPrec :: Int -> Constraint a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Constraint a -> ShowS
Show, (forall x. Constraint a -> Rep (Constraint a) x)
-> (forall x. Rep (Constraint a) x -> Constraint a)
-> Generic (Constraint a)
forall x. Rep (Constraint a) x -> Constraint a
forall x. Constraint a -> Rep (Constraint a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Constraint a) x -> Constraint a
forall a x. Constraint a -> Rep (Constraint a) x
$cto :: forall a x. Rep (Constraint a) x -> Constraint a
$cfrom :: forall a x. Constraint a -> Rep (Constraint a) x
Generic, a -> Constraint b -> Constraint a
(a -> b) -> Constraint a -> Constraint b
(forall a b. (a -> b) -> Constraint a -> Constraint b)
-> (forall a b. a -> Constraint b -> Constraint a)
-> Functor Constraint
forall a b. a -> Constraint b -> Constraint a
forall a b. (a -> b) -> Constraint a -> Constraint b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Constraint b -> Constraint a
$c<$ :: forall a b. a -> Constraint b -> Constraint a
fmap :: (a -> b) -> Constraint a -> Constraint b
$cfmap :: forall a b. (a -> b) -> Constraint a -> Constraint b
Functor, Constraint a -> Bool
(a -> m) -> Constraint a -> m
(a -> b -> b) -> b -> Constraint a -> b
(forall m. Monoid m => Constraint m -> m)
-> (forall m a. Monoid m => (a -> m) -> Constraint a -> m)
-> (forall m a. Monoid m => (a -> m) -> Constraint a -> m)
-> (forall a b. (a -> b -> b) -> b -> Constraint a -> b)
-> (forall a b. (a -> b -> b) -> b -> Constraint a -> b)
-> (forall b a. (b -> a -> b) -> b -> Constraint a -> b)
-> (forall b a. (b -> a -> b) -> b -> Constraint a -> b)
-> (forall a. (a -> a -> a) -> Constraint a -> a)
-> (forall a. (a -> a -> a) -> Constraint a -> a)
-> (forall a. Constraint a -> [a])
-> (forall a. Constraint a -> Bool)
-> (forall a. Constraint a -> Int)
-> (forall a. Eq a => a -> Constraint a -> Bool)
-> (forall a. Ord a => Constraint a -> a)
-> (forall a. Ord a => Constraint a -> a)
-> (forall a. Num a => Constraint a -> a)
-> (forall a. Num a => Constraint a -> a)
-> Foldable Constraint
forall a. Eq a => a -> Constraint a -> Bool
forall a. Num a => Constraint a -> a
forall a. Ord a => Constraint a -> a
forall m. Monoid m => Constraint m -> m
forall a. Constraint a -> Bool
forall a. Constraint a -> Int
forall a. Constraint a -> [a]
forall a. (a -> a -> a) -> Constraint a -> a
forall m a. Monoid m => (a -> m) -> Constraint a -> m
forall b a. (b -> a -> b) -> b -> Constraint a -> b
forall a b. (a -> b -> b) -> b -> Constraint a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Constraint a -> a
$cproduct :: forall a. Num a => Constraint a -> a
sum :: Constraint a -> a
$csum :: forall a. Num a => Constraint a -> a
minimum :: Constraint a -> a
$cminimum :: forall a. Ord a => Constraint a -> a
maximum :: Constraint a -> a
$cmaximum :: forall a. Ord a => Constraint a -> a
elem :: a -> Constraint a -> Bool
$celem :: forall a. Eq a => a -> Constraint a -> Bool
length :: Constraint a -> Int
$clength :: forall a. Constraint a -> Int
null :: Constraint a -> Bool
$cnull :: forall a. Constraint a -> Bool
toList :: Constraint a -> [a]
$ctoList :: forall a. Constraint a -> [a]
foldl1 :: (a -> a -> a) -> Constraint a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Constraint a -> a
foldr1 :: (a -> a -> a) -> Constraint a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Constraint a -> a
foldl' :: (b -> a -> b) -> b -> Constraint a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Constraint a -> b
foldl :: (b -> a -> b) -> b -> Constraint a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Constraint a -> b
foldr' :: (a -> b -> b) -> b -> Constraint a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Constraint a -> b
foldr :: (a -> b -> b) -> b -> Constraint a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Constraint a -> b
foldMap' :: (a -> m) -> Constraint a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Constraint a -> m
foldMap :: (a -> m) -> Constraint a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Constraint a -> m
fold :: Constraint m -> m
$cfold :: forall m. Monoid m => Constraint m -> m
Foldable, Functor Constraint
Foldable Constraint
Functor Constraint
-> Foldable Constraint
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Constraint a -> f (Constraint b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Constraint (f a) -> f (Constraint a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Constraint a -> m (Constraint b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Constraint (m a) -> m (Constraint a))
-> Traversable Constraint
(a -> f b) -> Constraint a -> f (Constraint 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 =>
Constraint (m a) -> m (Constraint a)
forall (f :: * -> *) a.
Applicative f =>
Constraint (f a) -> f (Constraint a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Constraint a -> m (Constraint b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Constraint a -> f (Constraint b)
sequence :: Constraint (m a) -> m (Constraint a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
Constraint (m a) -> m (Constraint a)
mapM :: (a -> m b) -> Constraint a -> m (Constraint b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Constraint a -> m (Constraint b)
sequenceA :: Constraint (f a) -> f (Constraint a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Constraint (f a) -> f (Constraint a)
traverse :: (a -> f b) -> Constraint a -> f (Constraint b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Constraint a -> f (Constraint b)
$cp2Traversable :: Foldable Constraint
$cp1Traversable :: Functor Constraint
Traversable)

instance NFData a => NFData (Constraint a)
instance Serialise a => Serialise (Constraint a)

srcConstraint :: Qualified (ProperName 'ClassName) -> [SourceType] -> [SourceType] -> Maybe ConstraintData -> SourceConstraint
srcConstraint :: Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> Maybe ConstraintData
-> SourceConstraint
srcConstraint = SourceAnn
-> Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> Maybe ConstraintData
-> SourceConstraint
forall a.
a
-> Qualified (ProperName 'ClassName)
-> [Type a]
-> [Type a]
-> Maybe ConstraintData
-> Constraint a
Constraint SourceAnn
NullSourceAnn

mapConstraintArgs :: ([Type a] -> [Type a]) -> Constraint a -> Constraint a
mapConstraintArgs :: ([Type a] -> [Type a]) -> Constraint a -> Constraint a
mapConstraintArgs [Type a] -> [Type a]
f Constraint a
c = Constraint a
c { constraintArgs :: [Type a]
constraintArgs = [Type a] -> [Type a]
f (Constraint a -> [Type a]
forall a. Constraint a -> [Type a]
constraintArgs Constraint a
c) }

overConstraintArgs :: Functor f => ([Type a] -> f [Type a]) -> Constraint a -> f (Constraint a)
overConstraintArgs :: ([Type a] -> f [Type a]) -> Constraint a -> f (Constraint a)
overConstraintArgs [Type a] -> f [Type a]
f Constraint a
c = (\[Type a]
args -> Constraint a
c { constraintArgs :: [Type a]
constraintArgs = [Type a]
args }) ([Type a] -> Constraint a) -> f [Type a] -> f (Constraint a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type a] -> f [Type a]
f (Constraint a -> [Type a]
forall a. Constraint a -> [Type a]
constraintArgs Constraint a
c)

mapConstraintKindArgs :: ([Type a] -> [Type a]) -> Constraint a -> Constraint a
mapConstraintKindArgs :: ([Type a] -> [Type a]) -> Constraint a -> Constraint a
mapConstraintKindArgs [Type a] -> [Type a]
f Constraint a
c = Constraint a
c { constraintKindArgs :: [Type a]
constraintKindArgs = [Type a] -> [Type a]
f (Constraint a -> [Type a]
forall a. Constraint a -> [Type a]
constraintKindArgs Constraint a
c) }

overConstraintKindArgs :: Functor f => ([Type a] -> f [Type a]) -> Constraint a -> f (Constraint a)
overConstraintKindArgs :: ([Type a] -> f [Type a]) -> Constraint a -> f (Constraint a)
overConstraintKindArgs [Type a] -> f [Type a]
f Constraint a
c = (\[Type a]
args -> Constraint a
c { constraintKindArgs :: [Type a]
constraintKindArgs = [Type a]
args }) ([Type a] -> Constraint a) -> f [Type a] -> f (Constraint a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type a] -> f [Type a]
f (Constraint a -> [Type a]
forall a. Constraint a -> [Type a]
constraintKindArgs Constraint a
c)

mapConstraintArgsAll :: ([Type a] -> [Type a]) -> Constraint a -> Constraint a
mapConstraintArgsAll :: ([Type a] -> [Type a]) -> Constraint a -> Constraint a
mapConstraintArgsAll [Type a] -> [Type a]
f Constraint a
c =
  Constraint a
c { constraintKindArgs :: [Type a]
constraintKindArgs = [Type a] -> [Type a]
f (Constraint a -> [Type a]
forall a. Constraint a -> [Type a]
constraintKindArgs Constraint a
c)
    , constraintArgs :: [Type a]
constraintArgs = [Type a] -> [Type a]
f (Constraint a -> [Type a]
forall a. Constraint a -> [Type a]
constraintArgs Constraint a
c)
    }

overConstraintArgsAll :: Applicative f => ([Type a] -> f [Type a]) -> Constraint a -> f (Constraint a)
overConstraintArgsAll :: ([Type a] -> f [Type a]) -> Constraint a -> f (Constraint a)
overConstraintArgsAll [Type a] -> f [Type a]
f Constraint a
c =
  (\[Type a]
a [Type a]
b -> Constraint a
c { constraintKindArgs :: [Type a]
constraintKindArgs = [Type a]
a, constraintArgs :: [Type a]
constraintArgs = [Type a]
b })
    ([Type a] -> [Type a] -> Constraint a)
-> f [Type a] -> f ([Type a] -> Constraint a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type a] -> f [Type a]
f (Constraint a -> [Type a]
forall a. Constraint a -> [Type a]
constraintKindArgs Constraint a
c)
    f ([Type a] -> Constraint a) -> f [Type a] -> f (Constraint a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Type a] -> f [Type a]
f (Constraint a -> [Type a]
forall a. Constraint a -> [Type a]
constraintArgs Constraint a
c)

constraintDataToJSON :: ConstraintData -> A.Value
constraintDataToJSON :: ConstraintData -> Value
constraintDataToJSON (PartialConstraintData [[Text]]
bs Bool
trunc) =
  [Pair] -> Value
A.object
    [ Text
"contents" Text -> ([[Text]], Bool) -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= ([[Text]]
bs, Bool
trunc)
    ]

constraintToJSON :: (a -> A.Value) -> Constraint a -> A.Value
constraintToJSON :: (a -> Value) -> Constraint a -> Value
constraintToJSON a -> Value
annToJSON (Constraint {a
[Type a]
Maybe ConstraintData
Qualified (ProperName 'ClassName)
constraintData :: Maybe ConstraintData
constraintArgs :: [Type a]
constraintKindArgs :: [Type a]
constraintClass :: Qualified (ProperName 'ClassName)
constraintAnn :: a
constraintData :: forall a. Constraint a -> Maybe ConstraintData
constraintArgs :: forall a. Constraint a -> [Type a]
constraintKindArgs :: forall a. Constraint a -> [Type a]
constraintClass :: forall a. Constraint a -> Qualified (ProperName 'ClassName)
constraintAnn :: forall a. Constraint a -> a
..}) =
  [Pair] -> Value
A.object
    [ Text
"constraintAnn"   Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= a -> Value
annToJSON a
constraintAnn
    , Text
"constraintClass" Text -> Qualified (ProperName 'ClassName) -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Qualified (ProperName 'ClassName)
constraintClass
    , Text
"constraintKindArgs"  Text -> [Value] -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= (Type a -> Value) -> [Type a] -> [Value]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Value) -> Type a -> Value
forall a. (a -> Value) -> Type a -> Value
typeToJSON a -> Value
annToJSON) [Type a]
constraintKindArgs
    , Text
"constraintArgs"  Text -> [Value] -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= (Type a -> Value) -> [Type a] -> [Value]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Value) -> Type a -> Value
forall a. (a -> Value) -> Type a -> Value
typeToJSON a -> Value
annToJSON) [Type a]
constraintArgs
    , Text
"constraintData"  Text -> Maybe Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= (ConstraintData -> Value) -> Maybe ConstraintData -> Maybe Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ConstraintData -> Value
constraintDataToJSON Maybe ConstraintData
constraintData
    ]

typeToJSON :: forall a. (a -> A.Value) -> Type a -> A.Value
typeToJSON :: (a -> Value) -> Type a -> Value
typeToJSON a -> Value
annToJSON Type a
ty =
  case Type a
ty of
    TUnknown a
a Int
b ->
      String -> a -> Int -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"TUnknown" a
a Int
b
    TypeVar a
a Text
b ->
      String -> a -> Text -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"TypeVar" a
a Text
b
    TypeLevelString a
a PSString
b ->
      String -> a -> PSString -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"TypeLevelString" a
a PSString
b
    TypeWildcard a
a Maybe Text
b ->
      String -> a -> Maybe Text -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"TypeWildcard" a
a Maybe Text
b
    TypeConstructor a
a Qualified (ProperName 'TypeName)
b ->
      String -> a -> Qualified (ProperName 'TypeName) -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"TypeConstructor" a
a Qualified (ProperName 'TypeName)
b
    TypeOp a
a Qualified (OpName 'TypeOpName)
b ->
      String -> a -> Qualified (OpName 'TypeOpName) -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"TypeOp" a
a Qualified (OpName 'TypeOpName)
b
    TypeApp a
a Type a
b Type a
c ->
      String -> a -> (Value, Value) -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"TypeApp" a
a (Type a -> Value
go Type a
b, Type a -> Value
go Type a
c)
    KindApp a
a Type a
b Type a
c ->
      String -> a -> (Value, Value) -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"KindApp" a
a (Type a -> Value
go Type a
b, Type a -> Value
go Type a
c)
    ForAll a
a Text
b Maybe (Type a)
c Type a
d Maybe SkolemScope
e ->
      case Maybe (Type a)
c of
        Maybe (Type a)
Nothing -> String -> a -> (Text, Value, Maybe SkolemScope) -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"ForAll" a
a (Text
b, Type a -> Value
go Type a
d, Maybe SkolemScope
e)
        Just Type a
k -> String -> a -> (Text, Value, Value, Maybe SkolemScope) -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"ForAll" a
a (Text
b, Type a -> Value
go Type a
k, Type a -> Value
go Type a
d, Maybe SkolemScope
e)
    ConstrainedType a
a Constraint a
b Type a
c ->
      String -> a -> (Value, Value) -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"ConstrainedType" a
a ((a -> Value) -> Constraint a -> Value
forall a. (a -> Value) -> Constraint a -> Value
constraintToJSON a -> Value
annToJSON Constraint a
b, Type a -> Value
go Type a
c)
    Skolem a
a Text
b Maybe (Type a)
c Int
d SkolemScope
e ->
      String -> a -> (Text, Maybe Value, Int, SkolemScope) -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"Skolem" a
a (Text
b, Type a -> Value
go (Type a -> Value) -> Maybe (Type a) -> Maybe Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Type a)
c, Int
d, SkolemScope
e)
    REmpty a
a ->
      String -> a -> Value
nullary String
"REmpty" a
a
    RCons a
a Label
b Type a
c Type a
d ->
      String -> a -> (Label, Value, Value) -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"RCons" a
a (Label
b, Type a -> Value
go Type a
c, Type a -> Value
go Type a
d)
    KindedType a
a Type a
b Type a
c ->
      String -> a -> (Value, Value) -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"KindedType" a
a (Type a -> Value
go Type a
b, Type a -> Value
go Type a
c)
    BinaryNoParensType a
a Type a
b Type a
c Type a
d ->
      String -> a -> (Value, Value, Value) -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"BinaryNoParensType" a
a (Type a -> Value
go Type a
b, Type a -> Value
go Type a
c, Type a -> Value
go Type a
d)
    ParensInType a
a Type a
b ->
      String -> a -> Value -> Value
forall b. ToJSON b => String -> a -> b -> Value
variant String
"ParensInType" a
a (Type a -> Value
go Type a
b)
  where
  go :: Type a -> A.Value
  go :: Type a -> Value
go = (a -> Value) -> Type a -> Value
forall a. (a -> Value) -> Type a -> Value
typeToJSON a -> Value
annToJSON

  variant :: A.ToJSON b => String -> a -> b -> A.Value
  variant :: String -> a -> b -> Value
variant String
tag a
ann b
contents =
    [Pair] -> Value
A.object
      [ Text
"tag"        Text -> String -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= String
tag
      , Text
"annotation" Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= a -> Value
annToJSON a
ann
      , Text
"contents"   Text -> b -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= b
contents
      ]

  nullary :: String -> a -> A.Value
  nullary :: String -> a -> Value
nullary String
tag a
ann =
    [Pair] -> Value
A.object
      [ Text
"tag"        Text -> String -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= String
tag
      , Text
"annotation" Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= a -> Value
annToJSON a
ann
      ]

instance A.ToJSON a => A.ToJSON (Type a) where
  toJSON :: Type a -> Value
toJSON = (a -> Value) -> Type a -> Value
forall a. (a -> Value) -> Type a -> Value
typeToJSON a -> Value
forall a. ToJSON a => a -> Value
A.toJSON

instance A.ToJSON a => A.ToJSON (Constraint a) where
  toJSON :: Constraint a -> Value
toJSON = (a -> Value) -> Constraint a -> Value
forall a. (a -> Value) -> Constraint a -> Value
constraintToJSON a -> Value
forall a. ToJSON a => a -> Value
A.toJSON

instance A.ToJSON ConstraintData where
  toJSON :: ConstraintData -> Value
toJSON = ConstraintData -> Value
constraintDataToJSON

constraintDataFromJSON :: A.Value -> A.Parser ConstraintData
constraintDataFromJSON :: Value -> Parser ConstraintData
constraintDataFromJSON = String
-> (Object -> Parser ConstraintData)
-> Value
-> Parser ConstraintData
forall a. String -> (Object -> Parser a) -> Value -> Parser a
A.withObject String
"PartialConstraintData" ((Object -> Parser ConstraintData)
 -> Value -> Parser ConstraintData)
-> (Object -> Parser ConstraintData)
-> Value
-> Parser ConstraintData
forall a b. (a -> b) -> a -> b
$ \Object
o -> do
  ([[Text]]
bs, Bool
trunc) <- Object
o Object -> Text -> Parser ([[Text]], Bool)
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"contents"
  ConstraintData -> Parser ConstraintData
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ConstraintData -> Parser ConstraintData)
-> ConstraintData -> Parser ConstraintData
forall a b. (a -> b) -> a -> b
$ [[Text]] -> Bool -> ConstraintData
PartialConstraintData [[Text]]
bs Bool
trunc

constraintFromJSON :: forall a. A.Parser a -> (A.Value -> A.Parser a) -> A.Value -> A.Parser (Constraint a)
constraintFromJSON :: Parser a -> (Value -> Parser a) -> Value -> Parser (Constraint a)
constraintFromJSON Parser a
defaultAnn Value -> Parser a
annFromJSON = String
-> (Object -> Parser (Constraint a))
-> Value
-> Parser (Constraint a)
forall a. String -> (Object -> Parser a) -> Value -> Parser a
A.withObject String
"Constraint" ((Object -> Parser (Constraint a))
 -> Value -> Parser (Constraint a))
-> (Object -> Parser (Constraint a))
-> Value
-> Parser (Constraint a)
forall a b. (a -> b) -> a -> b
$ \Object
o -> do
  a
constraintAnn   <- (Object
o Object -> Text -> Parser Value
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"constraintAnn" Parser Value -> (Value -> Parser a) -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Value -> Parser a
annFromJSON) Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser a
defaultAnn
  Qualified (ProperName 'ClassName)
constraintClass <- Object
o Object -> Text -> Parser (Qualified (ProperName 'ClassName))
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"constraintClass"
  [Type a]
constraintKindArgs <- Object
o Object -> Text -> Parser (Maybe [Value])
forall a. FromJSON a => Object -> Text -> Parser (Maybe a)
.:? Text
"constraintKindArgs" Parser (Maybe [Value]) -> [Value] -> Parser [Value]
forall a. Parser (Maybe a) -> a -> Parser a
.!= [] Parser [Value] -> ([Value] -> Parser [Type a]) -> Parser [Type a]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Value -> Parser (Type a)) -> [Value] -> Parser [Type a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
typeFromJSON Parser a
defaultAnn Value -> Parser a
annFromJSON)
  [Type a]
constraintArgs  <- Object
o Object -> Text -> Parser [Value]
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"constraintArgs" Parser [Value] -> ([Value] -> Parser [Type a]) -> Parser [Type a]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Value -> Parser (Type a)) -> [Value] -> Parser [Type a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
typeFromJSON Parser a
defaultAnn Value -> Parser a
annFromJSON)
  Maybe ConstraintData
constraintData  <- Object
o Object -> Text -> Parser (Maybe Value)
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"constraintData" Parser (Maybe Value)
-> (Maybe Value -> Parser (Maybe ConstraintData))
-> Parser (Maybe ConstraintData)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Value -> Parser ConstraintData)
-> Maybe Value -> Parser (Maybe ConstraintData)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Value -> Parser ConstraintData
constraintDataFromJSON
  Constraint a -> Parser (Constraint a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Constraint a -> Parser (Constraint a))
-> Constraint a -> Parser (Constraint a)
forall a b. (a -> b) -> a -> b
$ Constraint :: forall a.
a
-> Qualified (ProperName 'ClassName)
-> [Type a]
-> [Type a]
-> Maybe ConstraintData
-> Constraint a
Constraint {a
[Type a]
Maybe ConstraintData
Qualified (ProperName 'ClassName)
constraintData :: Maybe ConstraintData
constraintArgs :: [Type a]
constraintKindArgs :: [Type a]
constraintClass :: Qualified (ProperName 'ClassName)
constraintAnn :: a
constraintData :: Maybe ConstraintData
constraintArgs :: [Type a]
constraintKindArgs :: [Type a]
constraintClass :: Qualified (ProperName 'ClassName)
constraintAnn :: a
..}

typeFromJSON :: forall a. A.Parser a -> (A.Value -> A.Parser a) -> A.Value -> A.Parser (Type a)
typeFromJSON :: Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
typeFromJSON Parser a
defaultAnn Value -> Parser a
annFromJSON = String -> (Object -> Parser (Type a)) -> Value -> Parser (Type a)
forall a. String -> (Object -> Parser a) -> Value -> Parser a
A.withObject String
"Type" ((Object -> Parser (Type a)) -> Value -> Parser (Type a))
-> (Object -> Parser (Type a)) -> Value -> Parser (Type a)
forall a b. (a -> b) -> a -> b
$ \Object
o -> do
  String
tag <- Object
o Object -> Text -> Parser String
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"tag"
  a
a   <- (Object
o Object -> Text -> Parser Value
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"annotation" Parser Value -> (Value -> Parser a) -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Value -> Parser a
annFromJSON) Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser a
defaultAnn
  let
    contents :: A.FromJSON b => A.Parser b
    contents :: Parser b
contents = Object
o Object -> Text -> Parser b
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"contents"
  case String
tag of
    String
"TUnknown" ->
      a -> Int -> Type a
forall a. a -> Int -> Type a
TUnknown a
a (Int -> Type a) -> Parser Int -> Parser (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Int
forall b. FromJSON b => Parser b
contents
    String
"TypeVar" ->
      a -> Text -> Type a
forall a. a -> Text -> Type a
TypeVar a
a (Text -> Type a) -> Parser Text -> Parser (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text
forall b. FromJSON b => Parser b
contents
    String
"TypeLevelString" ->
      a -> PSString -> Type a
forall a. a -> PSString -> Type a
TypeLevelString a
a (PSString -> Type a) -> Parser PSString -> Parser (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser PSString
forall b. FromJSON b => Parser b
contents
    String
"TypeWildcard" -> do
      Maybe Text
b <- Parser (Maybe Text)
forall b. FromJSON b => Parser b
contents Parser (Maybe Text) -> Parser (Maybe Text) -> Parser (Maybe Text)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe Text -> Parser (Maybe Text)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Text
forall a. Maybe a
Nothing
      Type a -> Parser (Type a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type a -> Parser (Type a)) -> Type a -> Parser (Type a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe Text -> Type a
forall a. a -> Maybe Text -> Type a
TypeWildcard a
a Maybe Text
b
    String
"TypeConstructor" ->
      a -> Qualified (ProperName 'TypeName) -> Type a
forall a. a -> Qualified (ProperName 'TypeName) -> Type a
TypeConstructor a
a (Qualified (ProperName 'TypeName) -> Type a)
-> Parser (Qualified (ProperName 'TypeName)) -> Parser (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Qualified (ProperName 'TypeName))
forall b. FromJSON b => Parser b
contents
    String
"TypeOp" ->
      a -> Qualified (OpName 'TypeOpName) -> Type a
forall a. a -> Qualified (OpName 'TypeOpName) -> Type a
TypeOp a
a (Qualified (OpName 'TypeOpName) -> Type a)
-> Parser (Qualified (OpName 'TypeOpName)) -> Parser (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Qualified (OpName 'TypeOpName))
forall b. FromJSON b => Parser b
contents
    String
"TypeApp" -> do
      (Value
b, Value
c) <- Parser (Value, Value)
forall b. FromJSON b => Parser b
contents
      a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
TypeApp a
a (Type a -> Type a -> Type a)
-> Parser (Type a) -> Parser (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
b Parser (Type a -> Type a) -> Parser (Type a) -> Parser (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser (Type a)
go Value
c
    String
"KindApp" -> do
      (Value
b, Value
c) <- Parser (Value, Value)
forall b. FromJSON b => Parser b
contents
      a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindApp a
a (Type a -> Type a -> Type a)
-> Parser (Type a) -> Parser (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
b Parser (Type a -> Type a) -> Parser (Type a) -> Parser (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser (Type a)
go Value
c
    String
"ForAll" -> do
      let
        withoutMbKind :: Parser (Type a)
withoutMbKind = do
          (Text
b, Value
c, Maybe SkolemScope
d) <- Parser (Text, Value, Maybe SkolemScope)
forall b. FromJSON b => Parser b
contents
          a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
a Text
b Maybe (Type a)
forall a. Maybe a
Nothing (Type a -> Maybe SkolemScope -> Type a)
-> Parser (Type a) -> Parser (Maybe SkolemScope -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
c Parser (Maybe SkolemScope -> Type a)
-> Parser (Maybe SkolemScope) -> Parser (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe SkolemScope -> Parser (Maybe SkolemScope)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe SkolemScope
d
        withMbKind :: Parser (Type a)
withMbKind = do
          (Text
b, Value
c, Value
d, Maybe SkolemScope
e) <- Parser (Text, Value, Value, Maybe SkolemScope)
forall b. FromJSON b => Parser b
contents
          a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
a Text
b (Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a)
-> Parser (Maybe (Type a))
-> Parser (Type a -> Maybe SkolemScope -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type a -> Maybe (Type a)
forall a. a -> Maybe a
Just (Type a -> Maybe (Type a))
-> Parser (Type a) -> Parser (Maybe (Type a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
c) Parser (Type a -> Maybe SkolemScope -> Type a)
-> Parser (Type a) -> Parser (Maybe SkolemScope -> Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser (Type a)
go Value
d Parser (Maybe SkolemScope -> Type a)
-> Parser (Maybe SkolemScope) -> Parser (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe SkolemScope -> Parser (Maybe SkolemScope)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe SkolemScope
e
      Parser (Type a)
withMbKind Parser (Type a) -> Parser (Type a) -> Parser (Type a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (Type a)
withoutMbKind
    String
"ConstrainedType" -> do
      (Value
b, Value
c) <- Parser (Value, Value)
forall b. FromJSON b => Parser b
contents
      a -> Constraint a -> Type a -> Type a
forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
a (Constraint a -> Type a -> Type a)
-> Parser (Constraint a) -> Parser (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser a -> (Value -> Parser a) -> Value -> Parser (Constraint a)
forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Constraint a)
constraintFromJSON Parser a
defaultAnn Value -> Parser a
annFromJSON Value
b Parser (Type a -> Type a) -> Parser (Type a) -> Parser (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser (Type a)
go Value
c
    String
"Skolem" -> do
      (Text
b, Maybe Value
c, Int
d, SkolemScope
e) <- Parser (Text, Maybe Value, Int, SkolemScope)
forall b. FromJSON b => Parser b
contents
      Maybe (Type a)
c' <- (Value -> Parser (Type a))
-> Maybe Value -> Parser (Maybe (Type a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Value -> Parser (Type a)
go Maybe Value
c
      Type a -> Parser (Type a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type a -> Parser (Type a)) -> Type a -> Parser (Type a)
forall a b. (a -> b) -> a -> b
$ a -> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a
forall a.
a -> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a
Skolem a
a Text
b Maybe (Type a)
c' Int
d SkolemScope
e
    String
"REmpty" ->
      Type a -> Parser (Type a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type a -> Parser (Type a)) -> Type a -> Parser (Type a)
forall a b. (a -> b) -> a -> b
$ a -> Type a
forall a. a -> Type a
REmpty a
a
    String
"RCons" -> do
      (Label
b, Value
c, Value
d) <- Parser (Label, Value, Value)
forall b. FromJSON b => Parser b
contents
      a -> Label -> Type a -> Type a -> Type a
forall a. a -> Label -> Type a -> Type a -> Type a
RCons a
a Label
b (Type a -> Type a -> Type a)
-> Parser (Type a) -> Parser (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
c Parser (Type a -> Type a) -> Parser (Type a) -> Parser (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser (Type a)
go Value
d
    String
"KindedType" -> do
      (Value
b, Value
c) <- Parser (Value, Value)
forall b. FromJSON b => Parser b
contents
      a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindedType a
a (Type a -> Type a -> Type a)
-> Parser (Type a) -> Parser (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
b Parser (Type a -> Type a) -> Parser (Type a) -> Parser (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser (Type a)
go Value
c
    String
"BinaryNoParensType" -> do
      (Value
b, Value
c, Value
d) <- Parser (Value, Value, Value)
forall b. FromJSON b => Parser b
contents
      a -> Type a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a -> Type a
BinaryNoParensType a
a (Type a -> Type a -> Type a -> Type a)
-> Parser (Type a) -> Parser (Type a -> Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
b Parser (Type a -> Type a -> Type a)
-> Parser (Type a) -> Parser (Type a -> Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser (Type a)
go Value
c Parser (Type a -> Type a) -> Parser (Type a) -> Parser (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser (Type a)
go Value
d
    String
"ParensInType" -> do
      Value
b <- Parser Value
forall b. FromJSON b => Parser b
contents
      a -> Type a -> Type a
forall a. a -> Type a -> Type a
ParensInType a
a (Type a -> Type a) -> Parser (Type a) -> Parser (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
b
    -- Backwards compatability for kinds
    String
"KUnknown" ->
      a -> Int -> Type a
forall a. a -> Int -> Type a
TUnknown a
a (Int -> Type a) -> Parser Int -> Parser (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Int
forall b. FromJSON b => Parser b
contents
    String
"Row" ->
      a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
TypeApp a
a (a -> Qualified (ProperName 'TypeName) -> Type a
forall a. a -> Qualified (ProperName 'TypeName) -> Type a
TypeConstructor a
a Qualified (ProperName 'TypeName)
C.Row) (Type a -> Type a) -> Parser (Type a) -> Parser (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Parser (Type a)
go (Value -> Parser (Type a)) -> Parser Value -> Parser (Type a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Parser Value
forall b. FromJSON b => Parser b
contents)
    String
"FunKind" -> do
      (Value
b, Value
c) <- Parser (Value, Value)
forall b. FromJSON b => Parser b
contents
      a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
TypeApp a
a (Type a -> Type a -> Type a)
-> (Type a -> Type a) -> Type a -> Type a -> Type a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
TypeApp a
a (a -> Qualified (ProperName 'TypeName) -> Type a
forall a. a -> Qualified (ProperName 'TypeName) -> Type a
TypeConstructor a
a Qualified (ProperName 'TypeName)
C.Function) (Type a -> Type a -> Type a)
-> Parser (Type a) -> Parser (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
b Parser (Type a -> Type a) -> Parser (Type a) -> Parser (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser (Type a)
go Value
c
    String
"NamedKind" ->
      a -> Qualified (ProperName 'TypeName) -> Type a
forall a. a -> Qualified (ProperName 'TypeName) -> Type a
TypeConstructor a
a (Qualified (ProperName 'TypeName) -> Type a)
-> Parser (Qualified (ProperName 'TypeName)) -> Parser (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Qualified (ProperName 'TypeName))
forall b. FromJSON b => Parser b
contents
    String
other ->
      String -> Parser (Type a)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Parser (Type a)) -> String -> Parser (Type a)
forall a b. (a -> b) -> a -> b
$ String
"Unrecognised tag: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
other
  where
  go :: A.Value -> A.Parser (Type a)
  go :: Value -> Parser (Type a)
go = Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
typeFromJSON Parser a
defaultAnn Value -> Parser a
annFromJSON

-- These overlapping instances exist to preserve compatibility for common
-- instances which have a sensible default for missing annotations.
instance {-# OVERLAPPING #-} A.FromJSON (Type SourceAnn) where
  parseJSON :: Value -> Parser SourceType
parseJSON = Parser SourceAnn
-> (Value -> Parser SourceAnn) -> Value -> Parser SourceType
forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
typeFromJSON (SourceAnn -> Parser SourceAnn
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceAnn
NullSourceAnn) Value -> Parser SourceAnn
forall a. FromJSON a => Value -> Parser a
A.parseJSON

instance {-# OVERLAPPING #-} A.FromJSON (Type ()) where
  parseJSON :: Value -> Parser (Type ())
parseJSON = Parser () -> (Value -> Parser ()) -> Value -> Parser (Type ())
forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
typeFromJSON (() -> Parser ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) Value -> Parser ()
forall a. FromJSON a => Value -> Parser a
A.parseJSON

instance {-# OVERLAPPING #-} A.FromJSON a => A.FromJSON (Type a) where
  parseJSON :: Value -> Parser (Type a)
parseJSON = Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
typeFromJSON (String -> Parser a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Invalid annotation") Value -> Parser a
forall a. FromJSON a => Value -> Parser a
A.parseJSON

instance {-# OVERLAPPING #-} A.FromJSON (Constraint SourceAnn) where
  parseJSON :: Value -> Parser SourceConstraint
parseJSON = Parser SourceAnn
-> (Value -> Parser SourceAnn) -> Value -> Parser SourceConstraint
forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Constraint a)
constraintFromJSON (SourceAnn -> Parser SourceAnn
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceAnn
NullSourceAnn) Value -> Parser SourceAnn
forall a. FromJSON a => Value -> Parser a
A.parseJSON

instance {-# OVERLAPPING #-} A.FromJSON (Constraint ()) where
  parseJSON :: Value -> Parser (Constraint ())
parseJSON = Parser ()
-> (Value -> Parser ()) -> Value -> Parser (Constraint ())
forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Constraint a)
constraintFromJSON (() -> Parser ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) Value -> Parser ()
forall a. FromJSON a => Value -> Parser a
A.parseJSON

instance {-# OVERLAPPING #-} A.FromJSON a => A.FromJSON (Constraint a) where
  parseJSON :: Value -> Parser (Constraint a)
parseJSON = Parser a -> (Value -> Parser a) -> Value -> Parser (Constraint a)
forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Constraint a)
constraintFromJSON (String -> Parser a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Invalid annotation") Value -> Parser a
forall a. FromJSON a => Value -> Parser a
A.parseJSON

instance A.FromJSON ConstraintData where
  parseJSON :: Value -> Parser ConstraintData
parseJSON = Value -> Parser ConstraintData
constraintDataFromJSON

data RowListItem a = RowListItem
  { RowListItem a -> a
rowListAnn :: a
  , RowListItem a -> Label
rowListLabel :: Label
  , RowListItem a -> Type a
rowListType :: Type a
  } deriving (Int -> RowListItem a -> ShowS
[RowListItem a] -> ShowS
RowListItem a -> String
(Int -> RowListItem a -> ShowS)
-> (RowListItem a -> String)
-> ([RowListItem a] -> ShowS)
-> Show (RowListItem a)
forall a. Show a => Int -> RowListItem a -> ShowS
forall a. Show a => [RowListItem a] -> ShowS
forall a. Show a => RowListItem a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RowListItem a] -> ShowS
$cshowList :: forall a. Show a => [RowListItem a] -> ShowS
show :: RowListItem a -> String
$cshow :: forall a. Show a => RowListItem a -> String
showsPrec :: Int -> RowListItem a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> RowListItem a -> ShowS
Show, (forall x. RowListItem a -> Rep (RowListItem a) x)
-> (forall x. Rep (RowListItem a) x -> RowListItem a)
-> Generic (RowListItem a)
forall x. Rep (RowListItem a) x -> RowListItem a
forall x. RowListItem a -> Rep (RowListItem a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (RowListItem a) x -> RowListItem a
forall a x. RowListItem a -> Rep (RowListItem a) x
$cto :: forall a x. Rep (RowListItem a) x -> RowListItem a
$cfrom :: forall a x. RowListItem a -> Rep (RowListItem a) x
Generic, a -> RowListItem b -> RowListItem a
(a -> b) -> RowListItem a -> RowListItem b
(forall a b. (a -> b) -> RowListItem a -> RowListItem b)
-> (forall a b. a -> RowListItem b -> RowListItem a)
-> Functor RowListItem
forall a b. a -> RowListItem b -> RowListItem a
forall a b. (a -> b) -> RowListItem a -> RowListItem b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> RowListItem b -> RowListItem a
$c<$ :: forall a b. a -> RowListItem b -> RowListItem a
fmap :: (a -> b) -> RowListItem a -> RowListItem b
$cfmap :: forall a b. (a -> b) -> RowListItem a -> RowListItem b
Functor, RowListItem a -> Bool
(a -> m) -> RowListItem a -> m
(a -> b -> b) -> b -> RowListItem a -> b
(forall m. Monoid m => RowListItem m -> m)
-> (forall m a. Monoid m => (a -> m) -> RowListItem a -> m)
-> (forall m a. Monoid m => (a -> m) -> RowListItem a -> m)
-> (forall a b. (a -> b -> b) -> b -> RowListItem a -> b)
-> (forall a b. (a -> b -> b) -> b -> RowListItem a -> b)
-> (forall b a. (b -> a -> b) -> b -> RowListItem a -> b)
-> (forall b a. (b -> a -> b) -> b -> RowListItem a -> b)
-> (forall a. (a -> a -> a) -> RowListItem a -> a)
-> (forall a. (a -> a -> a) -> RowListItem a -> a)
-> (forall a. RowListItem a -> [a])
-> (forall a. RowListItem a -> Bool)
-> (forall a. RowListItem a -> Int)
-> (forall a. Eq a => a -> RowListItem a -> Bool)
-> (forall a. Ord a => RowListItem a -> a)
-> (forall a. Ord a => RowListItem a -> a)
-> (forall a. Num a => RowListItem a -> a)
-> (forall a. Num a => RowListItem a -> a)
-> Foldable RowListItem
forall a. Eq a => a -> RowListItem a -> Bool
forall a. Num a => RowListItem a -> a
forall a. Ord a => RowListItem a -> a
forall m. Monoid m => RowListItem m -> m
forall a. RowListItem a -> Bool
forall a. RowListItem a -> Int
forall a. RowListItem a -> [a]
forall a. (a -> a -> a) -> RowListItem a -> a
forall m a. Monoid m => (a -> m) -> RowListItem a -> m
forall b a. (b -> a -> b) -> b -> RowListItem a -> b
forall a b. (a -> b -> b) -> b -> RowListItem a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: RowListItem a -> a
$cproduct :: forall a. Num a => RowListItem a -> a
sum :: RowListItem a -> a
$csum :: forall a. Num a => RowListItem a -> a
minimum :: RowListItem a -> a
$cminimum :: forall a. Ord a => RowListItem a -> a
maximum :: RowListItem a -> a
$cmaximum :: forall a. Ord a => RowListItem a -> a
elem :: a -> RowListItem a -> Bool
$celem :: forall a. Eq a => a -> RowListItem a -> Bool
length :: RowListItem a -> Int
$clength :: forall a. RowListItem a -> Int
null :: RowListItem a -> Bool
$cnull :: forall a. RowListItem a -> Bool
toList :: RowListItem a -> [a]
$ctoList :: forall a. RowListItem a -> [a]
foldl1 :: (a -> a -> a) -> RowListItem a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> RowListItem a -> a
foldr1 :: (a -> a -> a) -> RowListItem a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> RowListItem a -> a
foldl' :: (b -> a -> b) -> b -> RowListItem a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> RowListItem a -> b
foldl :: (b -> a -> b) -> b -> RowListItem a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> RowListItem a -> b
foldr' :: (a -> b -> b) -> b -> RowListItem a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> RowListItem a -> b
foldr :: (a -> b -> b) -> b -> RowListItem a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> RowListItem a -> b
foldMap' :: (a -> m) -> RowListItem a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> RowListItem a -> m
foldMap :: (a -> m) -> RowListItem a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> RowListItem a -> m
fold :: RowListItem m -> m
$cfold :: forall m. Monoid m => RowListItem m -> m
Foldable, Functor RowListItem
Foldable RowListItem
Functor RowListItem
-> Foldable RowListItem
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RowListItem a -> f (RowListItem b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    RowListItem (f a) -> f (RowListItem a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> RowListItem a -> m (RowListItem b))
-> (forall (m :: * -> *) a.
    Monad m =>
    RowListItem (m a) -> m (RowListItem a))
-> Traversable RowListItem
(a -> f b) -> RowListItem a -> f (RowListItem 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 =>
RowListItem (m a) -> m (RowListItem a)
forall (f :: * -> *) a.
Applicative f =>
RowListItem (f a) -> f (RowListItem a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> RowListItem a -> m (RowListItem b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RowListItem a -> f (RowListItem b)
sequence :: RowListItem (m a) -> m (RowListItem a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
RowListItem (m a) -> m (RowListItem a)
mapM :: (a -> m b) -> RowListItem a -> m (RowListItem b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> RowListItem a -> m (RowListItem b)
sequenceA :: RowListItem (f a) -> f (RowListItem a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
RowListItem (f a) -> f (RowListItem a)
traverse :: (a -> f b) -> RowListItem a -> f (RowListItem b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RowListItem a -> f (RowListItem b)
$cp2Traversable :: Foldable RowListItem
$cp1Traversable :: Functor RowListItem
Traversable)

srcRowListItem :: Label -> SourceType -> RowListItem SourceAnn
srcRowListItem :: Label -> SourceType -> RowListItem SourceAnn
srcRowListItem = SourceAnn -> Label -> SourceType -> RowListItem SourceAnn
forall a. a -> Label -> Type a -> RowListItem a
RowListItem SourceAnn
NullSourceAnn

-- | Convert a row to a list of pairs of labels and types
rowToList :: Type a -> ([RowListItem a], Type a)
rowToList :: Type a -> ([RowListItem a], Type a)
rowToList = Type a -> ([RowListItem a], Type a)
forall a. Type a -> ([RowListItem a], Type a)
go where
  go :: Type a -> ([RowListItem a], Type a)
go (RCons a
ann Label
name Type a
ty Type a
row) =
    ([RowListItem a] -> [RowListItem a])
-> ([RowListItem a], Type a) -> ([RowListItem a], Type a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (a -> Label -> Type a -> RowListItem a
forall a. a -> Label -> Type a -> RowListItem a
RowListItem a
ann Label
name Type a
ty RowListItem a -> [RowListItem a] -> [RowListItem a]
forall a. a -> [a] -> [a]
:) (Type a -> ([RowListItem a], Type a)
forall a. Type a -> ([RowListItem a], Type a)
rowToList Type a
row)
  go Type a
r = ([], Type a
r)

-- | Convert a row to a list of pairs of labels and types, sorted by the labels.
rowToSortedList :: Type a -> ([RowListItem a], Type a)
rowToSortedList :: Type a -> ([RowListItem a], Type a)
rowToSortedList = ([RowListItem a] -> [RowListItem a])
-> ([RowListItem a], Type a) -> ([RowListItem a], Type a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((RowListItem a -> RowListItem a -> Ordering)
-> [RowListItem a] -> [RowListItem a]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((RowListItem a -> Label)
-> RowListItem a -> RowListItem a -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing RowListItem a -> Label
forall a. RowListItem a -> Label
rowListLabel)) (([RowListItem a], Type a) -> ([RowListItem a], Type a))
-> (Type a -> ([RowListItem a], Type a))
-> Type a
-> ([RowListItem a], Type a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type a -> ([RowListItem a], Type a)
forall a. Type a -> ([RowListItem a], Type a)
rowToList

-- | Convert a list of labels and types to a row
rowFromList :: ([RowListItem a], Type a) -> Type a
rowFromList :: ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem a]
xs, Type a
r) = (RowListItem a -> Type a -> Type a)
-> Type a -> [RowListItem a] -> Type a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(RowListItem a
ann Label
name Type a
ty) -> a -> Label -> Type a -> Type a -> Type a
forall a. a -> Label -> Type a -> Type a -> Type a
RCons a
ann Label
name Type a
ty) Type a
r [RowListItem a]
xs

-- | Align two rows of types, splitting them into three parts:
--
-- * Those types which appear in both rows
-- * Those which appear only on the left
-- * Those which appear only on the right
--
-- Note: importantly, we preserve the order of the types with a given label.
alignRowsWith
  :: (Type a -> Type a -> r)
  -> Type a
  -> Type a
  -> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith :: (Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith Type a -> Type a -> r
f Type a
ty1 Type a
ty2 = [RowListItem a]
-> [RowListItem a]
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
go [RowListItem a]
s1 [RowListItem a]
s2 where
  ([RowListItem a]
s1, Type a
tail1) = Type a -> ([RowListItem a], Type a)
forall a. Type a -> ([RowListItem a], Type a)
rowToSortedList Type a
ty1
  ([RowListItem a]
s2, Type a
tail2) = Type a -> ([RowListItem a], Type a)
forall a. Type a -> ([RowListItem a], Type a)
rowToSortedList Type a
ty2

  go :: [RowListItem a]
-> [RowListItem a]
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
go [] [RowListItem a]
r = ([], (([], Type a
tail1), ([RowListItem a]
r, Type a
tail2)))
  go [RowListItem a]
r [] = ([], (([RowListItem a]
r, Type a
tail1), ([], Type a
tail2)))
  go lhs :: [RowListItem a]
lhs@(RowListItem a
a1 Label
l1 Type a
t1 : [RowListItem a]
r1) rhs :: [RowListItem a]
rhs@(RowListItem a
a2 Label
l2 Type a
t2 : [RowListItem a]
r2)
    | Label
l1 Label -> Label -> Bool
forall a. Ord a => a -> a -> Bool
< Label
l2 = (((([RowListItem a], Type a), ([RowListItem a], Type a))
 -> (([RowListItem a], Type a), ([RowListItem a], Type a)))
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (((([RowListItem a], Type a), ([RowListItem a], Type a))
  -> (([RowListItem a], Type a), ([RowListItem a], Type a)))
 -> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
 -> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a))))
-> (([RowListItem a] -> [RowListItem a])
    -> (([RowListItem a], Type a), ([RowListItem a], Type a))
    -> (([RowListItem a], Type a), ([RowListItem a], Type a)))
-> ([RowListItem a] -> [RowListItem a])
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([RowListItem a], Type a) -> ([RowListItem a], Type a))
-> (([RowListItem a], Type a), ([RowListItem a], Type a))
-> (([RowListItem a], Type a), ([RowListItem a], Type a))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((([RowListItem a], Type a) -> ([RowListItem a], Type a))
 -> (([RowListItem a], Type a), ([RowListItem a], Type a))
 -> (([RowListItem a], Type a), ([RowListItem a], Type a)))
-> (([RowListItem a] -> [RowListItem a])
    -> ([RowListItem a], Type a) -> ([RowListItem a], Type a))
-> ([RowListItem a] -> [RowListItem a])
-> (([RowListItem a], Type a), ([RowListItem a], Type a))
-> (([RowListItem a], Type a), ([RowListItem a], Type a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([RowListItem a] -> [RowListItem a])
-> ([RowListItem a], Type a) -> ([RowListItem a], Type a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first) (a -> Label -> Type a -> RowListItem a
forall a. a -> Label -> Type a -> RowListItem a
RowListItem a
a1 Label
l1 Type a
t1 RowListItem a -> [RowListItem a] -> [RowListItem a]
forall a. a -> [a] -> [a]
:) ([RowListItem a]
-> [RowListItem a]
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
go [RowListItem a]
r1 [RowListItem a]
rhs)
    | Label
l2 Label -> Label -> Bool
forall a. Ord a => a -> a -> Bool
< Label
l1 = (((([RowListItem a], Type a), ([RowListItem a], Type a))
 -> (([RowListItem a], Type a), ([RowListItem a], Type a)))
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (((([RowListItem a], Type a), ([RowListItem a], Type a))
  -> (([RowListItem a], Type a), ([RowListItem a], Type a)))
 -> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
 -> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a))))
-> (([RowListItem a] -> [RowListItem a])
    -> (([RowListItem a], Type a), ([RowListItem a], Type a))
    -> (([RowListItem a], Type a), ([RowListItem a], Type a)))
-> ([RowListItem a] -> [RowListItem a])
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([RowListItem a], Type a) -> ([RowListItem a], Type a))
-> (([RowListItem a], Type a), ([RowListItem a], Type a))
-> (([RowListItem a], Type a), ([RowListItem a], Type a))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((([RowListItem a], Type a) -> ([RowListItem a], Type a))
 -> (([RowListItem a], Type a), ([RowListItem a], Type a))
 -> (([RowListItem a], Type a), ([RowListItem a], Type a)))
-> (([RowListItem a] -> [RowListItem a])
    -> ([RowListItem a], Type a) -> ([RowListItem a], Type a))
-> ([RowListItem a] -> [RowListItem a])
-> (([RowListItem a], Type a), ([RowListItem a], Type a))
-> (([RowListItem a], Type a), ([RowListItem a], Type a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([RowListItem a] -> [RowListItem a])
-> ([RowListItem a], Type a) -> ([RowListItem a], Type a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first) (a -> Label -> Type a -> RowListItem a
forall a. a -> Label -> Type a -> RowListItem a
RowListItem a
a2 Label
l2 Type a
t2 RowListItem a -> [RowListItem a] -> [RowListItem a]
forall a. a -> [a] -> [a]
:) ([RowListItem a]
-> [RowListItem a]
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
go [RowListItem a]
lhs [RowListItem a]
r2)
    | Bool
otherwise = ([r] -> [r])
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (Type a -> Type a -> r
f Type a
t1 Type a
t2 r -> [r] -> [r]
forall a. a -> [a] -> [a]
:) ([RowListItem a]
-> [RowListItem a]
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
go [RowListItem a]
r1 [RowListItem a]
r2)

-- | Check whether a type is a monotype
isMonoType :: Type a -> Bool
isMonoType :: Type a -> Bool
isMonoType ForAll{} = Bool
False
isMonoType (ParensInType a
_ Type a
t) = Type a -> Bool
forall a. Type a -> Bool
isMonoType Type a
t
isMonoType (KindedType a
_ Type a
t Type a
_) = Type a -> Bool
forall a. Type a -> Bool
isMonoType Type a
t
isMonoType Type a
_        = Bool
True

-- | Universally quantify a type
mkForAll :: [(a, (Text, Maybe (Type a)))] -> Type a -> Type a
mkForAll :: [(a, (Text, Maybe (Type a)))] -> Type a -> Type a
mkForAll [(a, (Text, Maybe (Type a)))]
args Type a
ty = ((a, (Text, Maybe (Type a))) -> Type a -> Type a)
-> Type a -> [(a, (Text, Maybe (Type a)))] -> Type a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(a
ann, (Text
arg, Maybe (Type a)
mbK)) Type a
t -> a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
arg Maybe (Type a)
mbK Type a
t Maybe SkolemScope
forall a. Maybe a
Nothing) Type a
ty [(a, (Text, Maybe (Type a)))]
args

-- | Replace a type variable, taking into account variable shadowing
replaceTypeVars :: Text -> Type a -> Type a -> Type a
replaceTypeVars :: Text -> Type a -> Type a -> Type a
replaceTypeVars Text
v Type a
r = [(Text, Type a)] -> Type a -> Type a
forall a. [(Text, Type a)] -> Type a -> Type a
replaceAllTypeVars [(Text
v, Type a
r)]

-- | Replace named type variables with types
replaceAllTypeVars :: [(Text, Type a)] -> Type a -> Type a
replaceAllTypeVars :: [(Text, Type a)] -> Type a -> Type a
replaceAllTypeVars = [Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [] where
  go :: [Text] -> [(Text, Type a)] -> Type a -> Type a
  go :: [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
_  [(Text, Type a)]
m (TypeVar a
ann Text
v) = Type a -> Maybe (Type a) -> Type a
forall a. a -> Maybe a -> a
fromMaybe (a -> Text -> Type a
forall a. a -> Text -> Type a
TypeVar a
ann Text
v) (Text
v Text -> [(Text, Type a)] -> Maybe (Type a)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(Text, Type a)]
m)
  go [Text]
bs [(Text, Type a)]
m (TypeApp a
ann Type a
t1 Type a
t2) = a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
TypeApp a
ann ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t1) ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t2)
  go [Text]
bs [(Text, Type a)]
m (KindApp a
ann Type a
t1 Type a
t2) = a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindApp a
ann ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t1) ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t2)
  go [Text]
bs [(Text, Type a)]
m (ForAll a
ann Text
v Maybe (Type a)
mbK Type a
t Maybe SkolemScope
sco)
    | Text
v Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
keys = [Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs (((Text, Type a) -> Bool) -> [(Text, Type a)] -> [(Text, Type a)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
/= Text
v) (Text -> Bool)
-> ((Text, Type a) -> Text) -> (Text, Type a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text, Type a) -> Text
forall a b. (a, b) -> a
fst) [(Text, Type a)]
m) (Type a -> Type a) -> Type a -> Type a
forall a b. (a -> b) -> a -> b
$ a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
v Maybe (Type a)
mbK' Type a
t Maybe SkolemScope
sco
    | Text
v Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
usedVars =
      let v' :: Text
v' = Text -> [Text] -> Text
forall (t :: * -> *). Foldable t => Text -> t Text -> Text
genName Text
v ([Text]
keys [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ [Text]
bs [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ [Text]
usedVars)
          t' :: Type a
t' = [Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text
v, a -> Text -> Type a
forall a. a -> Text -> Type a
TypeVar a
ann Text
v')] Type a
t
      in a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
v' Maybe (Type a)
mbK' ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go (Text
v' Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
bs) [(Text, Type a)]
m Type a
t') Maybe SkolemScope
sco
    | Bool
otherwise = a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
v Maybe (Type a)
mbK' ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go (Text
v Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
bs) [(Text, Type a)]
m Type a
t) Maybe SkolemScope
sco
    where
      mbK' :: Maybe (Type a)
mbK' = [Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m (Type a -> Type a) -> Maybe (Type a) -> Maybe (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Type a)
mbK
      keys :: [Text]
keys = ((Text, Type a) -> Text) -> [(Text, Type a)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Type a) -> Text
forall a b. (a, b) -> a
fst [(Text, Type a)]
m
      usedVars :: [Text]
usedVars = ((Text, Type a) -> [Text]) -> [(Text, Type a)] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Type a -> [Text]
forall a. Type a -> [Text]
usedTypeVariables (Type a -> [Text])
-> ((Text, Type a) -> Type a) -> (Text, Type a) -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text, Type a) -> Type a
forall a b. (a, b) -> b
snd) [(Text, Type a)]
m
  go [Text]
bs [(Text, Type a)]
m (ConstrainedType a
ann Constraint a
c Type a
t) = a -> Constraint a -> Type a -> Type a
forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
ann (([Type a] -> [Type a]) -> Constraint a -> Constraint a
forall a. ([Type a] -> [Type a]) -> Constraint a -> Constraint a
mapConstraintArgsAll ((Type a -> Type a) -> [Type a] -> [Type a]
forall a b. (a -> b) -> [a] -> [b]
map ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m)) Constraint a
c) ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t)
  go [Text]
bs [(Text, Type a)]
m (RCons a
ann Label
name' Type a
t Type a
r) = a -> Label -> Type a -> Type a -> Type a
forall a. a -> Label -> Type a -> Type a -> Type a
RCons a
ann Label
name' ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t) ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
r)
  go [Text]
bs [(Text, Type a)]
m (KindedType a
ann Type a
t Type a
k) = a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindedType a
ann ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t) ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
k)
  go [Text]
bs [(Text, Type a)]
m (BinaryNoParensType a
ann Type a
t1 Type a
t2 Type a
t3) = a -> Type a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a -> Type a
BinaryNoParensType a
ann ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t1) ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t2) ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t3)
  go [Text]
bs [(Text, Type a)]
m (ParensInType a
ann Type a
t) = a -> Type a -> Type a
forall a. a -> Type a -> Type a
ParensInType a
ann ([Text] -> [(Text, Type a)] -> Type a -> Type a
forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t)
  go [Text]
_  [(Text, Type a)]
_ Type a
ty = Type a
ty

  genName :: Text -> t Text -> Text
genName Text
orig t Text
inUse = Integer -> Text
try' Integer
0 where
    try' :: Integer -> Text
    try' :: Integer -> Text
try' Integer
n | (Text
orig Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Integer -> String
forall a. Show a => a -> String
show Integer
n)) Text -> t Text -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Text
inUse = Integer -> Text
try' (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
           | Bool
otherwise = Text
orig Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Integer -> String
forall a. Show a => a -> String
show Integer
n)

-- | Collect all type variables appearing in a type
usedTypeVariables :: Type a -> [Text]
usedTypeVariables :: Type a -> [Text]
usedTypeVariables = [Text] -> [Text]
forall a. Ord a => [a] -> [a]
ordNub ([Text] -> [Text]) -> (Type a -> [Text]) -> Type a -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Text] -> [Text] -> [Text])
-> (Type a -> [Text]) -> Type a -> [Text]
forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
(++) Type a -> [Text]
forall a. Type a -> [Text]
go where
  go :: Type a -> [Text]
go (TypeVar a
_ Text
v) = [Text
v]
  go Type a
_ = []

-- | Collect all free type variables appearing in a type
freeTypeVariables :: Type a -> [Text]
freeTypeVariables :: Type a -> [Text]
freeTypeVariables = [Text] -> [Text]
forall a. Ord a => [a] -> [a]
ordNub ([Text] -> [Text]) -> (Type a -> [Text]) -> Type a -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Text) -> Text) -> [(Int, Text)] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, Text) -> Text
forall a b. (a, b) -> b
snd ([(Int, Text)] -> [Text])
-> (Type a -> [(Int, Text)]) -> Type a -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Int, Text)] -> [(Int, Text)]
forall a. Ord a => [a] -> [a]
sort ([(Int, Text)] -> [(Int, Text)])
-> (Type a -> [(Int, Text)]) -> Type a -> [(Int, Text)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
0 [] where
  -- Tracks kind levels so that variables appearing in kind annotations are listed first.
  go :: Int -> [Text] -> Type a -> [(Int, Text)]
  go :: Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound (TypeVar a
_ Text
v) | Text
v Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Text]
bound = [(Int
lvl, Text
v)]
  go Int
lvl [Text]
bound (TypeApp a
_ Type a
t1 Type a
t2) = Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t1 [(Int, Text)] -> [(Int, Text)] -> [(Int, Text)]
forall a. [a] -> [a] -> [a]
++ Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t2
  go Int
lvl [Text]
bound (KindApp a
_ Type a
t1 Type a
t2) = Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t1 [(Int, Text)] -> [(Int, Text)] -> [(Int, Text)]
forall a. [a] -> [a] -> [a]
++ Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go (Int
lvl Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Text]
bound Type a
t2
  go Int
lvl [Text]
bound (ForAll a
_ Text
v Maybe (Type a)
mbK Type a
t Maybe SkolemScope
_) = (Type a -> [(Int, Text)]) -> Maybe (Type a) -> [(Int, Text)]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go (Int
lvl Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Text]
bound) Maybe (Type a)
mbK [(Int, Text)] -> [(Int, Text)] -> [(Int, Text)]
forall a. [a] -> [a] -> [a]
++ Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl (Text
v Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
bound) Type a
t
  go Int
lvl [Text]
bound (ConstrainedType a
_ Constraint a
c Type a
t) = (Type a -> [(Int, Text)]) -> [Type a] -> [(Int, Text)]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go (Int
lvl Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Text]
bound) (Constraint a -> [Type a]
forall a. Constraint a -> [Type a]
constraintKindArgs Constraint a
c) [(Int, Text)] -> [(Int, Text)] -> [(Int, Text)]
forall a. [a] -> [a] -> [a]
++ (Type a -> [(Int, Text)]) -> [Type a] -> [(Int, Text)]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound) (Constraint a -> [Type a]
forall a. Constraint a -> [Type a]
constraintArgs Constraint a
c) [(Int, Text)] -> [(Int, Text)] -> [(Int, Text)]
forall a. [a] -> [a] -> [a]
++ Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t
  go Int
lvl [Text]
bound (RCons a
_ Label
_ Type a
t Type a
r) = Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t [(Int, Text)] -> [(Int, Text)] -> [(Int, Text)]
forall a. [a] -> [a] -> [a]
++ Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
r
  go Int
lvl [Text]
bound (KindedType a
_ Type a
t Type a
k) = Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t [(Int, Text)] -> [(Int, Text)] -> [(Int, Text)]
forall a. [a] -> [a] -> [a]
++ Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go (Int
lvl Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Text]
bound Type a
k
  go Int
lvl [Text]
bound (BinaryNoParensType a
_ Type a
t1 Type a
t2 Type a
t3) = Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t1 [(Int, Text)] -> [(Int, Text)] -> [(Int, Text)]
forall a. [a] -> [a] -> [a]
++ Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t2 [(Int, Text)] -> [(Int, Text)] -> [(Int, Text)]
forall a. [a] -> [a] -> [a]
++ Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t3
  go Int
lvl [Text]
bound (ParensInType a
_ Type a
t) = Int -> [Text] -> Type a -> [(Int, Text)]
forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t
  go Int
_ [Text]
_ Type a
_ = []

-- | Collect a complete set of kind-annotated quantifiers at the front of a type.
completeBinderList :: Type a -> Maybe ([(a, (Text, Type a))], Type a)
completeBinderList :: Type a -> Maybe ([(a, (Text, Type a))], Type a)
completeBinderList = [(a, (Text, Type a))]
-> Type a -> Maybe ([(a, (Text, Type a))], Type a)
forall a.
[(a, (Text, Type a))]
-> Type a -> Maybe ([(a, (Text, Type a))], Type a)
go []
  where
  go :: [(a, (Text, Type a))]
-> Type a -> Maybe ([(a, (Text, Type a))], Type a)
go [(a, (Text, Type a))]
acc = \case
    ForAll a
_ Text
_ Maybe (Type a)
Nothing Type a
_ Maybe SkolemScope
_ -> Maybe ([(a, (Text, Type a))], Type a)
forall a. Maybe a
Nothing
    ForAll a
ann Text
var (Just Type a
k) Type a
ty Maybe SkolemScope
_ -> [(a, (Text, Type a))]
-> Type a -> Maybe ([(a, (Text, Type a))], Type a)
go ((a
ann, (Text
var, Type a
k)) (a, (Text, Type a))
-> [(a, (Text, Type a))] -> [(a, (Text, Type a))]
forall a. a -> [a] -> [a]
: [(a, (Text, Type a))]
acc) Type a
ty
    Type a
ty -> ([(a, (Text, Type a))], Type a)
-> Maybe ([(a, (Text, Type a))], Type a)
forall a. a -> Maybe a
Just ([(a, (Text, Type a))] -> [(a, (Text, Type a))]
forall a. [a] -> [a]
reverse [(a, (Text, Type a))]
acc, Type a
ty)

-- | Universally quantify over all type variables appearing free in a type
quantify :: Type a -> Type a
quantify :: Type a -> Type a
quantify Type a
ty = (Text -> Type a -> Type a) -> Type a -> [Text] -> Type a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Text
arg Type a
t -> a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll (Type a -> a
forall a. Type a -> a
getAnnForType Type a
ty) Text
arg Maybe (Type a)
forall a. Maybe a
Nothing Type a
t Maybe SkolemScope
forall a. Maybe a
Nothing) Type a
ty ([Text] -> Type a) -> [Text] -> Type a
forall a b. (a -> b) -> a -> b
$ Type a -> [Text]
forall a. Type a -> [Text]
freeTypeVariables Type a
ty

-- | Move all universal quantifiers to the front of a type
moveQuantifiersToFront :: Type a -> Type a
moveQuantifiersToFront :: Type a -> Type a
moveQuantifiersToFront = [(a, Text, Maybe SkolemScope, Maybe (Type a))]
-> [(a, Constraint a)] -> Type a -> Type a
forall a.
[(a, Text, Maybe SkolemScope, Maybe (Type a))]
-> [(a, Constraint a)] -> Type a -> Type a
go [] [] where
  go :: [(a, Text, Maybe SkolemScope, Maybe (Type a))]
-> [(a, Constraint a)] -> Type a -> Type a
go [(a, Text, Maybe SkolemScope, Maybe (Type a))]
qs [(a, Constraint a)]
cs (ForAll a
ann Text
q Maybe (Type a)
mbK Type a
ty Maybe SkolemScope
sco) = [(a, Text, Maybe SkolemScope, Maybe (Type a))]
-> [(a, Constraint a)] -> Type a -> Type a
go ((a
ann, Text
q, Maybe SkolemScope
sco, Maybe (Type a)
mbK) (a, Text, Maybe SkolemScope, Maybe (Type a))
-> [(a, Text, Maybe SkolemScope, Maybe (Type a))]
-> [(a, Text, Maybe SkolemScope, Maybe (Type a))]
forall a. a -> [a] -> [a]
: [(a, Text, Maybe SkolemScope, Maybe (Type a))]
qs) [(a, Constraint a)]
cs Type a
ty
  go [(a, Text, Maybe SkolemScope, Maybe (Type a))]
qs [(a, Constraint a)]
cs (ConstrainedType a
ann Constraint a
c Type a
ty) = [(a, Text, Maybe SkolemScope, Maybe (Type a))]
-> [(a, Constraint a)] -> Type a -> Type a
go [(a, Text, Maybe SkolemScope, Maybe (Type a))]
qs ((a
ann, Constraint a
c) (a, Constraint a) -> [(a, Constraint a)] -> [(a, Constraint a)]
forall a. a -> [a] -> [a]
: [(a, Constraint a)]
cs) Type a
ty
  go [(a, Text, Maybe SkolemScope, Maybe (Type a))]
qs [(a, Constraint a)]
cs Type a
ty = (Type a -> (a, Text, Maybe SkolemScope, Maybe (Type a)) -> Type a)
-> Type a
-> [(a, Text, Maybe SkolemScope, Maybe (Type a))]
-> Type a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Type a
ty' (a
ann, Text
q, Maybe SkolemScope
sco, Maybe (Type a)
mbK) -> a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
q Maybe (Type a)
mbK Type a
ty' Maybe SkolemScope
sco) ((Type a -> (a, Constraint a) -> Type a)
-> Type a -> [(a, Constraint a)] -> Type a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Type a
ty' (a
ann, Constraint a
c) -> a -> Constraint a -> Type a -> Type a
forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
ann Constraint a
c Type a
ty') Type a
ty [(a, Constraint a)]
cs) [(a, Text, Maybe SkolemScope, Maybe (Type a))]
qs

-- | Check if a type contains wildcards
containsWildcards :: Type a -> Bool
containsWildcards :: Type a -> Bool
containsWildcards = (Bool -> Bool -> Bool) -> (Type a -> Bool) -> Type a -> Bool
forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes Bool -> Bool -> Bool
(||) Type a -> Bool
forall a. Type a -> Bool
go where
  go :: Type a -> Bool
  go :: Type a -> Bool
go TypeWildcard{} = Bool
True
  go Type a
_ = Bool
False

-- | Check if a type contains `forall`
containsForAll :: Type a -> Bool
containsForAll :: Type a -> Bool
containsForAll = (Bool -> Bool -> Bool) -> (Type a -> Bool) -> Type a -> Bool
forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes Bool -> Bool -> Bool
(||) Type a -> Bool
forall a. Type a -> Bool
go where
  go :: Type a -> Bool
  go :: Type a -> Bool
go ForAll{} = Bool
True
  go Type a
_ = Bool
False

unknowns :: Type a -> IS.IntSet
unknowns :: Type a -> IntSet
unknowns = (IntSet -> IntSet -> IntSet)
-> (Type a -> IntSet) -> Type a -> IntSet
forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
(<>) Type a -> IntSet
forall a. Type a -> IntSet
go where
  go :: Type a -> IS.IntSet
  go :: Type a -> IntSet
go (TUnknown a
_ Int
u) = Int -> IntSet
IS.singleton Int
u
  go Type a
_ = IntSet
forall a. Monoid a => a
mempty

containsUnknowns :: Type a -> Bool
containsUnknowns :: Type a -> Bool
containsUnknowns = (Bool -> Bool -> Bool) -> (Type a -> Bool) -> Type a -> Bool
forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes Bool -> Bool -> Bool
(||) Type a -> Bool
forall a. Type a -> Bool
go where
  go :: Type a -> Bool
  go :: Type a -> Bool
go TUnknown{} = Bool
True
  go Type a
_ = Bool
False

eraseKindApps :: Type a -> Type a
eraseKindApps :: Type a -> Type a
eraseKindApps = (Type a -> Type a) -> Type a -> Type a
forall a. (Type a -> Type a) -> Type a -> Type a
everywhereOnTypes ((Type a -> Type a) -> Type a -> Type a)
-> (Type a -> Type a) -> Type a -> Type a
forall a b. (a -> b) -> a -> b
$ \case
  KindApp a
_ Type a
ty Type a
_ -> Type a
ty
  ConstrainedType a
ann Constraint a
con Type a
ty ->
    a -> Constraint a -> Type a -> Type a
forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
ann (Constraint a
con { constraintKindArgs :: [Type a]
constraintKindArgs = [] }) Type a
ty
  Type a
other -> Type a
other

eraseForAllKindAnnotations :: Type a -> Type a
eraseForAllKindAnnotations :: Type a -> Type a
eraseForAllKindAnnotations = Type a -> Type a
forall a. Type a -> Type a
removeAmbiguousVars (Type a -> Type a) -> (Type a -> Type a) -> Type a -> Type a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type a -> Type a
forall a. Type a -> Type a
removeForAllKinds
  where
  removeForAllKinds :: Type a -> Type a
removeForAllKinds = (Type a -> Type a) -> Type a -> Type a
forall a. (Type a -> Type a) -> Type a -> Type a
everywhereOnTypes ((Type a -> Type a) -> Type a -> Type a)
-> (Type a -> Type a) -> Type a -> Type a
forall a b. (a -> b) -> a -> b
$ \case
    ForAll a
ann Text
arg Maybe (Type a)
_ Type a
ty Maybe SkolemScope
sco ->
      a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
arg Maybe (Type a)
forall a. Maybe a
Nothing Type a
ty Maybe SkolemScope
sco
    Type a
other -> Type a
other

  removeAmbiguousVars :: Type a -> Type a
removeAmbiguousVars = (Type a -> Type a) -> Type a -> Type a
forall a. (Type a -> Type a) -> Type a -> Type a
everywhereOnTypes ((Type a -> Type a) -> Type a -> Type a)
-> (Type a -> Type a) -> Type a -> Type a
forall a b. (a -> b) -> a -> b
$ \case
    fa :: Type a
fa@(ForAll a
_ Text
arg Maybe (Type a)
_ Type a
ty Maybe SkolemScope
_)
      | Text
arg Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Type a -> [Text]
forall a. Type a -> [Text]
freeTypeVariables Type a
ty -> Type a
fa
      | Bool
otherwise -> Type a
ty
    Type a
other -> Type a
other

unapplyTypes :: Type a -> (Type a, [Type a], [Type a])
unapplyTypes :: Type a -> (Type a, [Type a], [Type a])
unapplyTypes = [Type a] -> Type a -> (Type a, [Type a], [Type a])
forall a. [Type a] -> Type a -> (Type a, [Type a], [Type a])
goTypes []
  where
  goTypes :: [Type a] -> Type a -> (Type a, [Type a], [Type a])
goTypes [Type a]
acc (TypeApp a
_ Type a
a Type a
b) = [Type a] -> Type a -> (Type a, [Type a], [Type a])
goTypes (Type a
b Type a -> [Type a] -> [Type a]
forall a. a -> [a] -> [a]
: [Type a]
acc) Type a
a
  goTypes [Type a]
acc Type a
a = let (Type a
ty, [Type a]
kinds) = [Type a] -> Type a -> (Type a, [Type a])
forall a. [Type a] -> Type a -> (Type a, [Type a])
goKinds [] Type a
a in (Type a
ty, [Type a]
kinds, [Type a]
acc)

  goKinds :: [Type a] -> Type a -> (Type a, [Type a])
goKinds [Type a]
acc (KindApp a
_ Type a
a Type a
b) = [Type a] -> Type a -> (Type a, [Type a])
goKinds (Type a
b Type a -> [Type a] -> [Type a]
forall a. a -> [a] -> [a]
: [Type a]
acc) Type a
a
  goKinds [Type a]
acc Type a
a = (Type a
a, [Type a]
acc)

unapplyConstraints :: Type a -> ([Constraint a], Type a)
unapplyConstraints :: Type a -> ([Constraint a], Type a)
unapplyConstraints = [Constraint a] -> Type a -> ([Constraint a], Type a)
forall a. [Constraint a] -> Type a -> ([Constraint a], Type a)
go []
  where
  go :: [Constraint a] -> Type a -> ([Constraint a], Type a)
go [Constraint a]
acc (ConstrainedType a
_ Constraint a
con Type a
ty) = [Constraint a] -> Type a -> ([Constraint a], Type a)
go (Constraint a
con Constraint a -> [Constraint a] -> [Constraint a]
forall a. a -> [a] -> [a]
: [Constraint a]
acc) Type a
ty
  go [Constraint a]
acc Type a
ty = ([Constraint a] -> [Constraint a]
forall a. [a] -> [a]
reverse [Constraint a]
acc, Type a
ty)

everywhereOnTypes :: (Type a -> Type a) -> Type a -> Type a
everywhereOnTypes :: (Type a -> Type a) -> Type a -> Type a
everywhereOnTypes Type a -> Type a
f = Type a -> Type a
go where
  go :: Type a -> Type a
go (TypeApp a
ann Type a
t1 Type a
t2) = Type a -> Type a
f (a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
TypeApp a
ann (Type a -> Type a
go Type a
t1) (Type a -> Type a
go Type a
t2))
  go (KindApp a
ann Type a
t1 Type a
t2) = Type a -> Type a
f (a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindApp a
ann (Type a -> Type a
go Type a
t1) (Type a -> Type a
go Type a
t2))
  go (ForAll a
ann Text
arg Maybe (Type a)
mbK Type a
ty Maybe SkolemScope
sco) = Type a -> Type a
f (a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
arg (Type a -> Type a
go (Type a -> Type a) -> Maybe (Type a) -> Maybe (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Type a)
mbK) (Type a -> Type a
go Type a
ty) Maybe SkolemScope
sco)
  go (ConstrainedType a
ann Constraint a
c Type a
ty) = Type a -> Type a
f (a -> Constraint a -> Type a -> Type a
forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
ann (([Type a] -> [Type a]) -> Constraint a -> Constraint a
forall a. ([Type a] -> [Type a]) -> Constraint a -> Constraint a
mapConstraintArgsAll ((Type a -> Type a) -> [Type a] -> [Type a]
forall a b. (a -> b) -> [a] -> [b]
map Type a -> Type a
go) (Constraint a -> Constraint a) -> Constraint a -> Constraint a
forall a b. (a -> b) -> a -> b
$ Constraint a
c) (Type a -> Type a
go Type a
ty))
  go (RCons a
ann Label
name Type a
ty Type a
rest) = Type a -> Type a
f (a -> Label -> Type a -> Type a -> Type a
forall a. a -> Label -> Type a -> Type a -> Type a
RCons a
ann Label
name (Type a -> Type a
go Type a
ty) (Type a -> Type a
go Type a
rest))
  go (KindedType a
ann Type a
ty Type a
k) = Type a -> Type a
f (a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindedType a
ann (Type a -> Type a
go Type a
ty) (Type a -> Type a
go Type a
k))
  go (BinaryNoParensType a
ann Type a
t1 Type a
t2 Type a
t3) = Type a -> Type a
f (a -> Type a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a -> Type a
BinaryNoParensType a
ann (Type a -> Type a
go Type a
t1) (Type a -> Type a
go Type a
t2) (Type a -> Type a
go Type a
t3))
  go (ParensInType a
ann Type a
t) = Type a -> Type a
f (a -> Type a -> Type a
forall a. a -> Type a -> Type a
ParensInType a
ann (Type a -> Type a
go Type a
t))
  go Type a
other = Type a -> Type a
f Type a
other

everywhereOnTypesTopDown :: (Type a -> Type a) -> Type a -> Type a
everywhereOnTypesTopDown :: (Type a -> Type a) -> Type a -> Type a
everywhereOnTypesTopDown Type a -> Type a
f = Type a -> Type a
go (Type a -> Type a) -> (Type a -> Type a) -> Type a -> Type a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type a -> Type a
f where
  go :: Type a -> Type a
go (TypeApp a
ann Type a
t1 Type a
t2) = a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
TypeApp a
ann (Type a -> Type a
go (Type a -> Type a
f Type a
t1)) (Type a -> Type a
go (Type a -> Type a
f Type a
t2))
  go (KindApp a
ann Type a
t1 Type a
t2) = a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindApp a
ann (Type a -> Type a
go (Type a -> Type a
f Type a
t1)) (Type a -> Type a
go (Type a -> Type a
f Type a
t2))
  go (ForAll a
ann Text
arg Maybe (Type a)
mbK Type a
ty Maybe SkolemScope
sco) = a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
arg (Type a -> Type a
go (Type a -> Type a) -> (Type a -> Type a) -> Type a -> Type a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type a -> Type a
f (Type a -> Type a) -> Maybe (Type a) -> Maybe (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Type a)
mbK) (Type a -> Type a
go (Type a -> Type a
f Type a
ty)) Maybe SkolemScope
sco
  go (ConstrainedType a
ann Constraint a
c Type a
ty) = a -> Constraint a -> Type a -> Type a
forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
ann (([Type a] -> [Type a]) -> Constraint a -> Constraint a
forall a. ([Type a] -> [Type a]) -> Constraint a -> Constraint a
mapConstraintArgsAll ((Type a -> Type a) -> [Type a] -> [Type a]
forall a b. (a -> b) -> [a] -> [b]
map (Type a -> Type a
go (Type a -> Type a) -> (Type a -> Type a) -> Type a -> Type a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type a -> Type a
f)) Constraint a
c) (Type a -> Type a
go (Type a -> Type a
f Type a
ty))
  go (RCons a
ann Label
name Type a
ty Type a
rest) = a -> Label -> Type a -> Type a -> Type a
forall a. a -> Label -> Type a -> Type a -> Type a
RCons a
ann Label
name (Type a -> Type a
go (Type a -> Type a
f Type a
ty)) (Type a -> Type a
go (Type a -> Type a
f Type a
rest))
  go (KindedType a
ann Type a
ty Type a
k) = a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindedType a
ann (Type a -> Type a
go (Type a -> Type a
f Type a
ty)) (Type a -> Type a
go (Type a -> Type a
f Type a
k))
  go (BinaryNoParensType a
ann Type a
t1 Type a
t2 Type a
t3) = a -> Type a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a -> Type a
BinaryNoParensType a
ann (Type a -> Type a
go (Type a -> Type a
f Type a
t1)) (Type a -> Type a
go (Type a -> Type a
f Type a
t2)) (Type a -> Type a
go (Type a -> Type a
f Type a
t3))
  go (ParensInType a
ann Type a
t) = a -> Type a -> Type a
forall a. a -> Type a -> Type a
ParensInType a
ann (Type a -> Type a
go (Type a -> Type a
f Type a
t))
  go Type a
other = Type a -> Type a
f Type a
other

everywhereOnTypesM :: Monad m => (Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereOnTypesM :: (Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereOnTypesM Type a -> m (Type a)
f = Type a -> m (Type a)
go where
  go :: Type a -> m (Type a)
go (TypeApp a
ann Type a
t1 Type a
t2) = (a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
TypeApp a
ann (Type a -> Type a -> Type a) -> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type a -> m (Type a)
go Type a
t1 m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
t2) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
f
  go (KindApp a
ann Type a
t1 Type a
t2) = (a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindApp a
ann (Type a -> Type a -> Type a) -> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type a -> m (Type a)
go Type a
t1 m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
t2) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
f
  go (ForAll a
ann Text
arg Maybe (Type a)
mbK Type a
ty Maybe SkolemScope
sco) = (a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
arg (Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a)
-> m (Maybe (Type a)) -> m (Type a -> Maybe SkolemScope -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type a -> m (Type a)) -> Maybe (Type a) -> m (Maybe (Type a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Type a -> m (Type a)
go Maybe (Type a)
mbK m (Type a -> Maybe SkolemScope -> Type a)
-> m (Type a) -> m (Maybe SkolemScope -> Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
ty m (Maybe SkolemScope -> Type a)
-> m (Maybe SkolemScope) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe SkolemScope -> m (Maybe SkolemScope)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe SkolemScope
sco) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
f
  go (ConstrainedType a
ann Constraint a
c Type a
ty) = (a -> Constraint a -> Type a -> Type a
forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
ann (Constraint a -> Type a -> Type a)
-> m (Constraint a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Type a] -> m [Type a]) -> Constraint a -> m (Constraint a)
forall (f :: * -> *) a.
Applicative f =>
([Type a] -> f [Type a]) -> Constraint a -> f (Constraint a)
overConstraintArgsAll ((Type a -> m (Type a)) -> [Type a] -> m [Type a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type a -> m (Type a)
go) Constraint a
c m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
ty) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
f
  go (RCons a
ann Label
name Type a
ty Type a
rest) = (a -> Label -> Type a -> Type a -> Type a
forall a. a -> Label -> Type a -> Type a -> Type a
RCons a
ann Label
name (Type a -> Type a -> Type a) -> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type a -> m (Type a)
go Type a
ty m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
rest) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
f
  go (KindedType a
ann Type a
ty Type a
k) = (a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindedType a
ann (Type a -> Type a -> Type a) -> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type a -> m (Type a)
go Type a
ty m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
k) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
f
  go (BinaryNoParensType a
ann Type a
t1 Type a
t2 Type a
t3) = (a -> Type a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a -> Type a
BinaryNoParensType a
ann (Type a -> Type a -> Type a -> Type a)
-> m (Type a) -> m (Type a -> Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type a -> m (Type a)
go Type a
t1 m (Type a -> Type a -> Type a)
-> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
t2 m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
t3) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
f
  go (ParensInType a
ann Type a
t) = (a -> Type a -> Type a
forall a. a -> Type a -> Type a
ParensInType a
ann (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type a -> m (Type a)
go Type a
t) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
f
  go Type a
other = Type a -> m (Type a)
f Type a
other

everywhereWithScopeOnTypesM :: Monad m => S.Set Text -> (S.Set Text -> Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereWithScopeOnTypesM :: Set Text
-> (Set Text -> Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereWithScopeOnTypesM Set Text
s0 Set Text -> Type a -> m (Type a)
f = Set Text -> Type a -> m (Type a)
go Set Text
s0 where
  go :: Set Text -> Type a -> m (Type a)
go Set Text
s (TypeApp a
ann Type a
t1 Type a
t2) = (a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
TypeApp a
ann (Type a -> Type a -> Type a) -> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Text -> Type a -> m (Type a)
go Set Text
s Type a
t1 m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Text -> Type a -> m (Type a)
go Set Text
s Type a
t2) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set Text -> Type a -> m (Type a)
f Set Text
s
  go Set Text
s (KindApp a
ann Type a
t1 Type a
t2) = (a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindApp a
ann (Type a -> Type a -> Type a) -> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Text -> Type a -> m (Type a)
go Set Text
s Type a
t1 m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Text -> Type a -> m (Type a)
go Set Text
s Type a
t2) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set Text -> Type a -> m (Type a)
f Set Text
s
  go Set Text
s (ForAll a
ann Text
arg Maybe (Type a)
mbK Type a
ty Maybe SkolemScope
sco) = (a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
arg (Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a)
-> m (Maybe (Type a)) -> m (Type a -> Maybe SkolemScope -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type a -> m (Type a)) -> Maybe (Type a) -> m (Maybe (Type a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Set Text -> Type a -> m (Type a)
go Set Text
s) Maybe (Type a)
mbK m (Type a -> Maybe SkolemScope -> Type a)
-> m (Type a) -> m (Maybe SkolemScope -> Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Text -> Type a -> m (Type a)
go (Text -> Set Text -> Set Text
forall a. Ord a => a -> Set a -> Set a
S.insert Text
arg Set Text
s) Type a
ty m (Maybe SkolemScope -> Type a)
-> m (Maybe SkolemScope) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe SkolemScope -> m (Maybe SkolemScope)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe SkolemScope
sco) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set Text -> Type a -> m (Type a)
f Set Text
s
  go Set Text
s (ConstrainedType a
ann Constraint a
c Type a
ty) = (a -> Constraint a -> Type a -> Type a
forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
ann (Constraint a -> Type a -> Type a)
-> m (Constraint a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Type a] -> m [Type a]) -> Constraint a -> m (Constraint a)
forall (f :: * -> *) a.
Applicative f =>
([Type a] -> f [Type a]) -> Constraint a -> f (Constraint a)
overConstraintArgsAll ((Type a -> m (Type a)) -> [Type a] -> m [Type a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Set Text -> Type a -> m (Type a)
go Set Text
s)) Constraint a
c m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Text -> Type a -> m (Type a)
go Set Text
s Type a
ty) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set Text -> Type a -> m (Type a)
f Set Text
s
  go Set Text
s (RCons a
ann Label
name Type a
ty Type a
rest) = (a -> Label -> Type a -> Type a -> Type a
forall a. a -> Label -> Type a -> Type a -> Type a
RCons a
ann Label
name (Type a -> Type a -> Type a) -> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Text -> Type a -> m (Type a)
go Set Text
s Type a
ty m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Text -> Type a -> m (Type a)
go Set Text
s Type a
rest) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set Text -> Type a -> m (Type a)
f Set Text
s
  go Set Text
s (KindedType a
ann Type a
ty Type a
k) = (a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindedType a
ann (Type a -> Type a -> Type a) -> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Text -> Type a -> m (Type a)
go Set Text
s Type a
ty m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Text -> Type a -> m (Type a)
go Set Text
s Type a
k) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set Text -> Type a -> m (Type a)
f Set Text
s
  go Set Text
s (BinaryNoParensType a
ann Type a
t1 Type a
t2 Type a
t3) = (a -> Type a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a -> Type a
BinaryNoParensType a
ann (Type a -> Type a -> Type a -> Type a)
-> m (Type a) -> m (Type a -> Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Text -> Type a -> m (Type a)
go Set Text
s Type a
t1 m (Type a -> Type a -> Type a)
-> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Text -> Type a -> m (Type a)
go Set Text
s Type a
t2 m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Text -> Type a -> m (Type a)
go Set Text
s Type a
t3) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set Text -> Type a -> m (Type a)
f Set Text
s
  go Set Text
s (ParensInType a
ann Type a
t) = (a -> Type a -> Type a
forall a. a -> Type a -> Type a
ParensInType a
ann (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Text -> Type a -> m (Type a)
go Set Text
s Type a
t) m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set Text -> Type a -> m (Type a)
f Set Text
s
  go Set Text
s Type a
other = Set Text -> Type a -> m (Type a)
f Set Text
s Type a
other

everywhereOnTypesTopDownM :: Monad m => (Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereOnTypesTopDownM :: (Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereOnTypesTopDownM Type a -> m (Type a)
f = Type a -> m (Type a)
go (Type a -> m (Type a))
-> (Type a -> m (Type a)) -> Type a -> m (Type a)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Type a -> m (Type a)
f where
  go :: Type a -> m (Type a)
go (TypeApp a
ann Type a
t1 Type a
t2) = a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
TypeApp a
ann (Type a -> Type a -> Type a) -> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type a -> m (Type a)
f Type a
t1 m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
go) m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type a -> m (Type a)
f Type a
t2 m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
go)
  go (KindApp a
ann Type a
t1 Type a
t2) = a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindApp a
ann (Type a -> Type a -> Type a) -> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type a -> m (Type a)
f Type a
t1 m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
go) m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type a -> m (Type a)
f Type a
t2 m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
go)
  go (ForAll a
ann Text
arg Maybe (Type a)
mbK Type a
ty Maybe SkolemScope
sco) = a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
arg (Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a)
-> m (Maybe (Type a)) -> m (Type a -> Maybe SkolemScope -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Type a -> m (Type a)) -> Maybe (Type a) -> m (Maybe (Type a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Type a -> m (Type a)
f (Type a -> m (Type a))
-> (Type a -> m (Type a)) -> Type a -> m (Type a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Type a -> m (Type a)
go) Maybe (Type a)
mbK) m (Type a -> Maybe SkolemScope -> Type a)
-> m (Type a) -> m (Maybe SkolemScope -> Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type a -> m (Type a)
f Type a
ty m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
go) m (Maybe SkolemScope -> Type a)
-> m (Maybe SkolemScope) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe SkolemScope -> m (Maybe SkolemScope)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe SkolemScope
sco
  go (ConstrainedType a
ann Constraint a
c Type a
ty) = a -> Constraint a -> Type a -> Type a
forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
ann (Constraint a -> Type a -> Type a)
-> m (Constraint a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Type a] -> m [Type a]) -> Constraint a -> m (Constraint a)
forall (f :: * -> *) a.
Applicative f =>
([Type a] -> f [Type a]) -> Constraint a -> f (Constraint a)
overConstraintArgsAll ((Type a -> m (Type a)) -> [Type a] -> m [Type a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type a -> m (Type a)
go (Type a -> m (Type a))
-> (Type a -> m (Type a)) -> Type a -> m (Type a)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Type a -> m (Type a)
f)) Constraint a
c m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type a -> m (Type a)
f Type a
ty m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
go)
  go (RCons a
ann Label
name Type a
ty Type a
rest) = a -> Label -> Type a -> Type a -> Type a
forall a. a -> Label -> Type a -> Type a -> Type a
RCons a
ann Label
name (Type a -> Type a -> Type a) -> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type a -> m (Type a)
f Type a
ty m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
go) m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type a -> m (Type a)
f Type a
rest m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
go)
  go (KindedType a
ann Type a
ty Type a
k) = a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindedType a
ann (Type a -> Type a -> Type a) -> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type a -> m (Type a)
f Type a
ty m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
go) m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type a -> m (Type a)
f Type a
k m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
go)
  go (BinaryNoParensType a
ann Type a
t1 Type a
t2 Type a
t3) = a -> Type a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a -> Type a
BinaryNoParensType a
ann (Type a -> Type a -> Type a -> Type a)
-> m (Type a) -> m (Type a -> Type a -> Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type a -> m (Type a)
f Type a
t1 m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
go) m (Type a -> Type a -> Type a)
-> m (Type a) -> m (Type a -> Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type a -> m (Type a)
f Type a
t2 m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
go) m (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type a -> m (Type a)
f Type a
t3 m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
go)
  go (ParensInType a
ann Type a
t) = a -> Type a -> Type a
forall a. a -> Type a -> Type a
ParensInType a
ann (Type a -> Type a) -> m (Type a) -> m (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type a -> m (Type a)
f Type a
t m (Type a) -> (Type a -> m (Type a)) -> m (Type a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
go)
  go Type a
other = Type a -> m (Type a)
f Type a
other

everythingOnTypes :: (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes :: (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes r -> r -> r
(<+>) Type a -> r
f = Type a -> r
go where
  go :: Type a -> r
go t :: Type a
t@(TypeApp a
_ Type a
t1 Type a
t2) = Type a -> r
f Type a
t r -> r -> r
<+> Type a -> r
go Type a
t1 r -> r -> r
<+> Type a -> r
go Type a
t2
  go t :: Type a
t@(KindApp a
_ Type a
t1 Type a
t2) = Type a -> r
f Type a
t r -> r -> r
<+> Type a -> r
go Type a
t1 r -> r -> r
<+> Type a -> r
go Type a
t2
  go t :: Type a
t@(ForAll a
_ Text
_ (Just Type a
k) Type a
ty Maybe SkolemScope
_) = Type a -> r
f Type a
t r -> r -> r
<+> Type a -> r
go Type a
k r -> r -> r
<+> Type a -> r
go Type a
ty
  go t :: Type a
t@(ForAll a
_ Text
_ Maybe (Type a)
_ Type a
ty Maybe SkolemScope
_) = Type a -> r
f Type a
t r -> r -> r
<+> Type a -> r
go Type a
ty
  go t :: Type a
t@(ConstrainedType a
_ Constraint a
c Type a
ty) = (r -> r -> r) -> r -> [r] -> r
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl r -> r -> r
(<+>) (Type a -> r
f Type a
t) ((Type a -> r) -> [Type a] -> [r]
forall a b. (a -> b) -> [a] -> [b]
map Type a -> r
go (Constraint a -> [Type a]
forall a. Constraint a -> [Type a]
constraintKindArgs Constraint a
c) [r] -> [r] -> [r]
forall a. [a] -> [a] -> [a]
++ (Type a -> r) -> [Type a] -> [r]
forall a b. (a -> b) -> [a] -> [b]
map Type a -> r
go (Constraint a -> [Type a]
forall a. Constraint a -> [Type a]
constraintArgs Constraint a
c)) r -> r -> r
<+> Type a -> r
go Type a
ty
  go t :: Type a
t@(RCons a
_ Label
_ Type a
ty Type a
rest) = Type a -> r
f Type a
t r -> r -> r
<+> Type a -> r
go Type a
ty r -> r -> r
<+> Type a -> r
go Type a
rest
  go t :: Type a
t@(KindedType a
_ Type a
ty Type a
k) = Type a -> r
f Type a
t r -> r -> r
<+> Type a -> r
go Type a
ty r -> r -> r
<+> Type a -> r
go Type a
k
  go t :: Type a
t@(BinaryNoParensType a
_ Type a
t1 Type a
t2 Type a
t3) = Type a -> r
f Type a
t r -> r -> r
<+> Type a -> r
go Type a
t1 r -> r -> r
<+> Type a -> r
go Type a
t2 r -> r -> r
<+> Type a -> r
go Type a
t3
  go t :: Type a
t@(ParensInType a
_ Type a
t1) = Type a -> r
f Type a
t r -> r -> r
<+> Type a -> r
go Type a
t1
  go Type a
other = Type a -> r
f Type a
other

everythingWithContextOnTypes :: s -> r -> (r -> r -> r) -> (s -> Type a -> (s, r)) -> Type a -> r
everythingWithContextOnTypes :: s -> r -> (r -> r -> r) -> (s -> Type a -> (s, r)) -> Type a -> r
everythingWithContextOnTypes s
s0 r
r0 r -> r -> r
(<+>) s -> Type a -> (s, r)
f = s -> Type a -> r
go' s
s0 where
  go' :: s -> Type a -> r
go' s
s Type a
t = let (s
s', r
r) = s -> Type a -> (s, r)
f s
s Type a
t in r
r r -> r -> r
<+> s -> Type a -> r
go s
s' Type a
t
  go :: s -> Type a -> r
go s
s (TypeApp a
_ Type a
t1 Type a
t2) = s -> Type a -> r
go' s
s Type a
t1 r -> r -> r
<+> s -> Type a -> r
go' s
s Type a
t2
  go s
s (KindApp a
_ Type a
t1 Type a
t2) = s -> Type a -> r
go' s
s Type a
t1 r -> r -> r
<+> s -> Type a -> r
go' s
s Type a
t2
  go s
s (ForAll a
_ Text
_ (Just Type a
k) Type a
ty Maybe SkolemScope
_) = s -> Type a -> r
go' s
s Type a
k r -> r -> r
<+> s -> Type a -> r
go' s
s Type a
ty
  go s
s (ForAll a
_ Text
_ Maybe (Type a)
_ Type a
ty Maybe SkolemScope
_) = s -> Type a -> r
go' s
s Type a
ty
  go s
s (ConstrainedType a
_ Constraint a
c Type a
ty) = (r -> r -> r) -> r -> [r] -> r
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl r -> r -> r
(<+>) r
r0 ((Type a -> r) -> [Type a] -> [r]
forall a b. (a -> b) -> [a] -> [b]
map (s -> Type a -> r
go' s
s) (Constraint a -> [Type a]
forall a. Constraint a -> [Type a]
constraintKindArgs Constraint a
c) [r] -> [r] -> [r]
forall a. [a] -> [a] -> [a]
++ (Type a -> r) -> [Type a] -> [r]
forall a b. (a -> b) -> [a] -> [b]
map (s -> Type a -> r
go' s
s) (Constraint a -> [Type a]
forall a. Constraint a -> [Type a]
constraintArgs Constraint a
c)) r -> r -> r
<+> s -> Type a -> r
go' s
s Type a
ty
  go s
s (RCons a
_ Label
_ Type a
ty Type a
rest) = s -> Type a -> r
go' s
s Type a
ty r -> r -> r
<+> s -> Type a -> r
go' s
s Type a
rest
  go s
s (KindedType a
_ Type a
ty Type a
k) = s -> Type a -> r
go' s
s Type a
ty r -> r -> r
<+> s -> Type a -> r
go' s
s Type a
k
  go s
s (BinaryNoParensType a
_ Type a
t1 Type a
t2 Type a
t3) = s -> Type a -> r
go' s
s Type a
t1 r -> r -> r
<+> s -> Type a -> r
go' s
s Type a
t2 r -> r -> r
<+> s -> Type a -> r
go' s
s Type a
t3
  go s
s (ParensInType a
_ Type a
t1) = s -> Type a -> r
go' s
s Type a
t1
  go s
_ Type a
_ = r
r0

annForType :: Lens' (Type a) a
annForType :: (a -> f a) -> Type a -> f (Type a)
annForType a -> f a
k (TUnknown a
a Int
b) = (\a
z -> a -> Int -> Type a
forall a. a -> Int -> Type a
TUnknown a
z Int
b) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (TypeVar a
a Text
b) = (\a
z -> a -> Text -> Type a
forall a. a -> Text -> Type a
TypeVar a
z Text
b) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (TypeLevelString a
a PSString
b) = (\a
z -> a -> PSString -> Type a
forall a. a -> PSString -> Type a
TypeLevelString a
z PSString
b) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (TypeWildcard a
a Maybe Text
b) = (\a
z -> a -> Maybe Text -> Type a
forall a. a -> Maybe Text -> Type a
TypeWildcard a
z Maybe Text
b) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (TypeConstructor a
a Qualified (ProperName 'TypeName)
b) = (\a
z -> a -> Qualified (ProperName 'TypeName) -> Type a
forall a. a -> Qualified (ProperName 'TypeName) -> Type a
TypeConstructor a
z Qualified (ProperName 'TypeName)
b) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (TypeOp a
a Qualified (OpName 'TypeOpName)
b) = (\a
z -> a -> Qualified (OpName 'TypeOpName) -> Type a
forall a. a -> Qualified (OpName 'TypeOpName) -> Type a
TypeOp a
z Qualified (OpName 'TypeOpName)
b) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (TypeApp a
a Type a
b Type a
c) = (\a
z -> a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
TypeApp a
z Type a
b Type a
c) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (KindApp a
a Type a
b Type a
c) = (\a
z -> a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindApp a
z Type a
b Type a
c) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (ForAll a
a Text
b Maybe (Type a)
c Type a
d Maybe SkolemScope
e) = (\a
z -> a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
z Text
b Maybe (Type a)
c Type a
d Maybe SkolemScope
e) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (ConstrainedType a
a Constraint a
b Type a
c) = (\a
z -> a -> Constraint a -> Type a -> Type a
forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
z Constraint a
b Type a
c) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (Skolem a
a Text
b Maybe (Type a)
c Int
d SkolemScope
e) = (\a
z -> a -> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a
forall a.
a -> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a
Skolem a
z Text
b Maybe (Type a)
c Int
d SkolemScope
e) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (REmpty a
a) = a -> Type a
forall a. a -> Type a
REmpty (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (RCons a
a Label
b Type a
c Type a
d) = (\a
z -> a -> Label -> Type a -> Type a -> Type a
forall a. a -> Label -> Type a -> Type a -> Type a
RCons a
z Label
b Type a
c Type a
d) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (KindedType a
a Type a
b Type a
c) = (\a
z -> a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a
KindedType a
z Type a
b Type a
c) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (BinaryNoParensType a
a Type a
b Type a
c Type a
d) = (\a
z -> a -> Type a -> Type a -> Type a -> Type a
forall a. a -> Type a -> Type a -> Type a -> Type a
BinaryNoParensType a
z Type a
b Type a
c Type a
d) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (ParensInType a
a Type a
b) = (\a
z -> a -> Type a -> Type a
forall a. a -> Type a -> Type a
ParensInType a
z Type a
b) (a -> Type a) -> f a -> f (Type a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a

getAnnForType :: Type a -> a
getAnnForType :: Type a -> a
getAnnForType = (Type a -> Getting a (Type a) a -> a
forall s a. s -> Getting a s a -> a
^. Getting a (Type a) a
forall a. Lens' (Type a) a
annForType)

setAnnForType :: a -> Type a -> Type a
setAnnForType :: a -> Type a -> Type a
setAnnForType = ASetter (Type a) (Type a) a a -> a -> Type a -> Type a
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter (Type a) (Type a) a a
forall a. Lens' (Type a) a
annForType

instance Eq (Type a) where
  == :: Type a -> Type a -> Bool
(==) = Type a -> Type a -> Bool
forall a b. Type a -> Type b -> Bool
eqType

instance Ord (Type a) where
  compare :: Type a -> Type a -> Ordering
compare = Type a -> Type a -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType

eqType :: Type a -> Type b -> Bool
eqType :: Type a -> Type b -> Bool
eqType (TUnknown a
_ Int
a) (TUnknown b
_ Int
a') = Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
a'
eqType (TypeVar a
_ Text
a) (TypeVar b
_ Text
a') = Text
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
a'
eqType (TypeLevelString a
_ PSString
a) (TypeLevelString b
_ PSString
a') = PSString
a PSString -> PSString -> Bool
forall a. Eq a => a -> a -> Bool
== PSString
a'
eqType (TypeWildcard a
_ Maybe Text
a) (TypeWildcard b
_ Maybe Text
a') = Maybe Text
a Maybe Text -> Maybe Text -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Text
a'
eqType (TypeConstructor a
_ Qualified (ProperName 'TypeName)
a) (TypeConstructor b
_ Qualified (ProperName 'TypeName)
a') = Qualified (ProperName 'TypeName)
a Qualified (ProperName 'TypeName)
-> Qualified (ProperName 'TypeName) -> Bool
forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
a'
eqType (TypeOp a
_ Qualified (OpName 'TypeOpName)
a) (TypeOp b
_ Qualified (OpName 'TypeOpName)
a') = Qualified (OpName 'TypeOpName)
a Qualified (OpName 'TypeOpName)
-> Qualified (OpName 'TypeOpName) -> Bool
forall a. Eq a => a -> a -> Bool
== Qualified (OpName 'TypeOpName)
a'
eqType (TypeApp a
_ Type a
a Type a
b) (TypeApp b
_ Type b
a' Type b
b') = Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
a Type b
a' Bool -> Bool -> Bool
&& Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
b Type b
b'
eqType (KindApp a
_ Type a
a Type a
b) (KindApp b
_ Type b
a' Type b
b') = Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
a Type b
a' Bool -> Bool -> Bool
&& Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
b Type b
b'
eqType (ForAll a
_ Text
a Maybe (Type a)
b Type a
c Maybe SkolemScope
d) (ForAll b
_ Text
a' Maybe (Type b)
b' Type b
c' Maybe SkolemScope
d') = Text
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
a' Bool -> Bool -> Bool
&& Maybe (Type a) -> Maybe (Type b) -> Bool
forall a b. Maybe (Type a) -> Maybe (Type b) -> Bool
eqMaybeType Maybe (Type a)
b Maybe (Type b)
b' Bool -> Bool -> Bool
&& Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
c Type b
c' Bool -> Bool -> Bool
&& Maybe SkolemScope
d Maybe SkolemScope -> Maybe SkolemScope -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe SkolemScope
d'
eqType (ConstrainedType a
_ Constraint a
a Type a
b) (ConstrainedType b
_ Constraint b
a' Type b
b') = Constraint a -> Constraint b -> Bool
forall a b. Constraint a -> Constraint b -> Bool
eqConstraint Constraint a
a Constraint b
a' Bool -> Bool -> Bool
&& Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
b Type b
b'
eqType (Skolem a
_ Text
a Maybe (Type a)
b Int
c SkolemScope
d) (Skolem b
_ Text
a' Maybe (Type b)
b' Int
c' SkolemScope
d') = Text
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
a' Bool -> Bool -> Bool
&& Maybe (Type a) -> Maybe (Type b) -> Bool
forall a b. Maybe (Type a) -> Maybe (Type b) -> Bool
eqMaybeType Maybe (Type a)
b Maybe (Type b)
b' Bool -> Bool -> Bool
&& Int
c Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
c' Bool -> Bool -> Bool
&& SkolemScope
d SkolemScope -> SkolemScope -> Bool
forall a. Eq a => a -> a -> Bool
== SkolemScope
d'
eqType (REmpty a
_) (REmpty b
_) = Bool
True
eqType (RCons a
_ Label
a Type a
b Type a
c) (RCons b
_ Label
a' Type b
b' Type b
c') = Label
a Label -> Label -> Bool
forall a. Eq a => a -> a -> Bool
== Label
a' Bool -> Bool -> Bool
&& Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
b Type b
b' Bool -> Bool -> Bool
&& Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
c Type b
c'
eqType (KindedType a
_ Type a
a Type a
b) (KindedType b
_ Type b
a' Type b
b') = Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
a Type b
a' Bool -> Bool -> Bool
&& Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
b Type b
b'
eqType (BinaryNoParensType a
_ Type a
a Type a
b Type a
c) (BinaryNoParensType b
_ Type b
a' Type b
b' Type b
c') = Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
a Type b
a' Bool -> Bool -> Bool
&& Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
b Type b
b' Bool -> Bool -> Bool
&& Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
c Type b
c'
eqType (ParensInType a
_ Type a
a) (ParensInType b
_ Type b
a') = Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
a Type b
a'
eqType Type a
_ Type b
_ = Bool
False

eqMaybeType :: Maybe (Type a) -> Maybe (Type b) -> Bool
eqMaybeType :: Maybe (Type a) -> Maybe (Type b) -> Bool
eqMaybeType (Just Type a
a) (Just Type b
b) = Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType Type a
a Type b
b
eqMaybeType Maybe (Type a)
Nothing Maybe (Type b)
Nothing = Bool
True
eqMaybeType Maybe (Type a)
_ Maybe (Type b)
_ = Bool
False

compareType :: Type a -> Type b -> Ordering
compareType :: Type a -> Type b -> Ordering
compareType (TUnknown a
_ Int
a) (TUnknown b
_ Int
a') = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
a Int
a'
compareType (TypeVar a
_ Text
a) (TypeVar b
_ Text
a') = Text -> Text -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Text
a Text
a'
compareType (TypeLevelString a
_ PSString
a) (TypeLevelString b
_ PSString
a') = PSString -> PSString -> Ordering
forall a. Ord a => a -> a -> Ordering
compare PSString
a PSString
a'
compareType (TypeWildcard a
_ Maybe Text
a) (TypeWildcard b
_ Maybe Text
a') = Maybe Text -> Maybe Text -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Maybe Text
a Maybe Text
a'
compareType (TypeConstructor a
_ Qualified (ProperName 'TypeName)
a) (TypeConstructor b
_ Qualified (ProperName 'TypeName)
a') = Qualified (ProperName 'TypeName)
-> Qualified (ProperName 'TypeName) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Qualified (ProperName 'TypeName)
a Qualified (ProperName 'TypeName)
a'
compareType (TypeOp a
_ Qualified (OpName 'TypeOpName)
a) (TypeOp b
_ Qualified (OpName 'TypeOpName)
a') = Qualified (OpName 'TypeOpName)
-> Qualified (OpName 'TypeOpName) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Qualified (OpName 'TypeOpName)
a Qualified (OpName 'TypeOpName)
a'
compareType (TypeApp a
_ Type a
a Type a
b) (TypeApp b
_ Type b
a' Type b
b') = Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
a Type b
a' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
b Type b
b'
compareType (KindApp a
_ Type a
a Type a
b) (KindApp b
_ Type b
a' Type b
b') = Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
a Type b
a' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
b Type b
b'
compareType (ForAll a
_ Text
a Maybe (Type a)
b Type a
c Maybe SkolemScope
d) (ForAll b
_ Text
a' Maybe (Type b)
b' Type b
c' Maybe SkolemScope
d') = Text -> Text -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Text
a Text
a' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Maybe (Type a) -> Maybe (Type b) -> Ordering
forall a b. Maybe (Type a) -> Maybe (Type b) -> Ordering
compareMaybeType Maybe (Type a)
b Maybe (Type b)
b' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
c Type b
c' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Maybe SkolemScope -> Maybe SkolemScope -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Maybe SkolemScope
d Maybe SkolemScope
d'
compareType (ConstrainedType a
_ Constraint a
a Type a
b) (ConstrainedType b
_ Constraint b
a' Type b
b') = Constraint a -> Constraint b -> Ordering
forall a b. Constraint a -> Constraint b -> Ordering
compareConstraint Constraint a
a Constraint b
a' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
b Type b
b'
compareType (Skolem a
_ Text
a Maybe (Type a)
b Int
c SkolemScope
d) (Skolem b
_ Text
a' Maybe (Type b)
b' Int
c' SkolemScope
d') = Text -> Text -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Text
a Text
a' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Maybe (Type a) -> Maybe (Type b) -> Ordering
forall a b. Maybe (Type a) -> Maybe (Type b) -> Ordering
compareMaybeType Maybe (Type a)
b Maybe (Type b)
b' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
c Int
c' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> SkolemScope -> SkolemScope -> Ordering
forall a. Ord a => a -> a -> Ordering
compare SkolemScope
d SkolemScope
d'
compareType (REmpty a
_) (REmpty b
_) = Ordering
EQ
compareType (RCons a
_ Label
a Type a
b Type a
c) (RCons b
_ Label
a' Type b
b' Type b
c') = Label -> Label -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Label
a Label
a' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
b Type b
b' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
c Type b
c'
compareType (KindedType a
_ Type a
a Type a
b) (KindedType b
_ Type b
a' Type b
b') = Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
a Type b
a' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
b Type b
b'
compareType (BinaryNoParensType a
_ Type a
a Type a
b Type a
c) (BinaryNoParensType b
_ Type b
a' Type b
b' Type b
c') = Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
a Type b
a' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
b Type b
b' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
c Type b
c'
compareType (ParensInType a
_ Type a
a) (ParensInType b
_ Type b
a') = Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
a Type b
a'
compareType Type a
typ Type b
typ' =
  Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Type a -> Int
forall a. Type a -> Int
orderOf Type a
typ) (Type b -> Int
forall a. Type a -> Int
orderOf Type b
typ')
    where
      orderOf :: Type a -> Int
      orderOf :: Type a -> Int
orderOf TUnknown{} = Int
0
      orderOf TypeVar{} = Int
1
      orderOf TypeLevelString{} = Int
2
      orderOf TypeWildcard{} = Int
3
      orderOf TypeConstructor{} = Int
4
      orderOf TypeOp{} = Int
5
      orderOf TypeApp{} = Int
6
      orderOf KindApp{} = Int
7
      orderOf ForAll{} = Int
8
      orderOf ConstrainedType{} = Int
9
      orderOf Skolem{} = Int
10
      orderOf REmpty{} = Int
11
      orderOf RCons{} = Int
12
      orderOf KindedType{} = Int
13
      orderOf BinaryNoParensType{} = Int
14
      orderOf ParensInType{} = Int
15

compareMaybeType :: Maybe (Type a) -> Maybe (Type b) -> Ordering
compareMaybeType :: Maybe (Type a) -> Maybe (Type b) -> Ordering
compareMaybeType (Just Type a
a) (Just Type b
b) = Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType Type a
a Type b
b
compareMaybeType Maybe (Type a)
Nothing Maybe (Type b)
Nothing = Ordering
EQ
compareMaybeType Maybe (Type a)
Nothing Maybe (Type b)
_ = Ordering
LT
compareMaybeType Maybe (Type a)
_ Maybe (Type b)
_ = Ordering
GT

instance Eq (Constraint a) where
  == :: Constraint a -> Constraint a -> Bool
(==) = Constraint a -> Constraint a -> Bool
forall a b. Constraint a -> Constraint b -> Bool
eqConstraint

instance Ord (Constraint a) where
  compare :: Constraint a -> Constraint a -> Ordering
compare = Constraint a -> Constraint a -> Ordering
forall a b. Constraint a -> Constraint b -> Ordering
compareConstraint

eqConstraint :: Constraint a -> Constraint b -> Bool
eqConstraint :: Constraint a -> Constraint b -> Bool
eqConstraint (Constraint a
_ Qualified (ProperName 'ClassName)
a [Type a]
b [Type a]
c Maybe ConstraintData
d) (Constraint b
_ Qualified (ProperName 'ClassName)
a' [Type b]
b' [Type b]
c' Maybe ConstraintData
d') = Qualified (ProperName 'ClassName)
a Qualified (ProperName 'ClassName)
-> Qualified (ProperName 'ClassName) -> Bool
forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'ClassName)
a' Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Type a -> Type b -> Bool) -> [Type a] -> [Type b] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType [Type a]
b [Type b]
b') Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Type a -> Type b -> Bool) -> [Type a] -> [Type b] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type a -> Type b -> Bool
forall a b. Type a -> Type b -> Bool
eqType [Type a]
c [Type b]
c') Bool -> Bool -> Bool
&& Maybe ConstraintData
d Maybe ConstraintData -> Maybe ConstraintData -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe ConstraintData
d'

compareConstraint :: Constraint a -> Constraint b -> Ordering
compareConstraint :: Constraint a -> Constraint b -> Ordering
compareConstraint (Constraint a
_ Qualified (ProperName 'ClassName)
a [Type a]
b [Type a]
c Maybe ConstraintData
d) (Constraint b
_ Qualified (ProperName 'ClassName)
a' [Type b]
b' [Type b]
c' Maybe ConstraintData
d') = Qualified (ProperName 'ClassName)
-> Qualified (ProperName 'ClassName) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Qualified (ProperName 'ClassName)
a Qualified (ProperName 'ClassName)
a' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> [Ordering] -> Ordering
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold ((Type a -> Type b -> Ordering)
-> [Type a] -> [Type b] -> [Ordering]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType [Type a]
b [Type b]
b') Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> [Ordering] -> Ordering
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold ((Type a -> Type b -> Ordering)
-> [Type a] -> [Type b] -> [Ordering]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type a -> Type b -> Ordering
forall a b. Type a -> Type b -> Ordering
compareType [Type a]
c [Type b]
c') Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Maybe ConstraintData -> Maybe ConstraintData -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Maybe ConstraintData
d Maybe ConstraintData
d'