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

import Prelude
import Protolude (ordNub)

import Codec.Serialise (Serialise)
import Control.Applicative ((<|>))
import Control.Arrow (first, second)
import Control.DeepSeq (NFData)
import Control.Lens (Lens', (^.), set)
import Control.Monad ((<=<), (>=>))
import Data.Aeson ((.:), (.:?), (.!=), (.=))
import Data.Aeson qualified as A
import Data.Aeson.Types qualified as A
import Data.Foldable (fold, foldl')
import Data.IntSet qualified as IS
import Data.List (sortOn)
import Data.Maybe (fromMaybe, isJust)
import Data.Text (Text)
import Data.Text qualified as T
import GHC.Generics (Generic)

import Language.PureScript.AST.SourcePos (pattern NullSourceAnn, SourceAnn, SourceSpan)
import Language.PureScript.Constants.Prim qualified as C
import Language.PureScript.Names (OpName, OpNameType(..), ProperName, ProperNameType(..), Qualified, coerceProperName)
import Language.PureScript.Label (Label)
import Language.PureScript.PSString (PSString)

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
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
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
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
Ord, [SkolemScope] -> Encoding
[SkolemScope] -> Value
SkolemScope -> Encoding
SkolemScope -> Value
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
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. 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

-- |
-- Describes how a TypeWildcard should be presented to the user during
-- type checking: holes (?foo) are always emitted as errors, whereas unnamed
-- wildcards (_) default to warnings, but are ignored entirely if they are
-- contained by a binding with a complete (wildcard-free) type signature.
--
data WildcardData = HoleWildcard Text | UnnamedWildcard | IgnoredWildcard
  deriving (Int -> WildcardData -> ShowS
[WildcardData] -> ShowS
WildcardData -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WildcardData] -> ShowS
$cshowList :: [WildcardData] -> ShowS
show :: WildcardData -> String
$cshow :: WildcardData -> String
showsPrec :: Int -> WildcardData -> ShowS
$cshowsPrec :: Int -> WildcardData -> ShowS
Show, WildcardData -> WildcardData -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WildcardData -> WildcardData -> Bool
$c/= :: WildcardData -> WildcardData -> Bool
== :: WildcardData -> WildcardData -> Bool
$c== :: WildcardData -> WildcardData -> Bool
Eq, Eq WildcardData
WildcardData -> WildcardData -> Bool
WildcardData -> WildcardData -> Ordering
WildcardData -> WildcardData -> WildcardData
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 :: WildcardData -> WildcardData -> WildcardData
$cmin :: WildcardData -> WildcardData -> WildcardData
max :: WildcardData -> WildcardData -> WildcardData
$cmax :: WildcardData -> WildcardData -> WildcardData
>= :: WildcardData -> WildcardData -> Bool
$c>= :: WildcardData -> WildcardData -> Bool
> :: WildcardData -> WildcardData -> Bool
$c> :: WildcardData -> WildcardData -> Bool
<= :: WildcardData -> WildcardData -> Bool
$c<= :: WildcardData -> WildcardData -> Bool
< :: WildcardData -> WildcardData -> Bool
$c< :: WildcardData -> WildcardData -> Bool
compare :: WildcardData -> WildcardData -> Ordering
$ccompare :: WildcardData -> WildcardData -> Ordering
Ord, forall x. Rep WildcardData x -> WildcardData
forall x. WildcardData -> Rep WildcardData x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep WildcardData x -> WildcardData
$cfrom :: forall x. WildcardData -> Rep WildcardData x
Generic)

instance NFData WildcardData
instance Serialise WildcardData

-- |
-- 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-level natural
  | TypeLevelInt a Integer
  -- | A type wildcard, as would appear in a partial type synonym
  | TypeWildcard a WildcardData
  -- | 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
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 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, 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
<$ :: forall a b. a -> Type b -> Type a
$c<$ :: forall a b. a -> Type b -> Type a
fmap :: forall a b. (a -> b) -> Type a -> Type b
$cfmap :: forall a b. (a -> b) -> Type a -> Type b
Functor, 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 :: forall a. Num a => Type a -> a
$cproduct :: forall a. Num a => Type a -> a
sum :: forall a. Num a => Type a -> a
$csum :: forall a. Num a => Type a -> a
minimum :: forall a. Ord a => Type a -> a
$cminimum :: forall a. Ord a => Type a -> a
maximum :: forall a. Ord a => Type a -> a
$cmaximum :: forall a. Ord a => Type a -> a
elem :: forall a. Eq a => a -> Type a -> Bool
$celem :: forall a. Eq a => a -> Type a -> Bool
length :: forall a. Type a -> Int
$clength :: forall a. Type a -> Int
null :: forall a. Type a -> Bool
$cnull :: forall a. Type a -> Bool
toList :: forall a. Type a -> [a]
$ctoList :: forall a. Type a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Type a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Type a -> a
foldr1 :: forall a. (a -> a -> a) -> Type a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Type a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Type a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Type a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Type a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Type a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Type a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Type a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Type a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Type a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Type a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Type a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Type a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Type a -> m
fold :: forall m. Monoid m => Type m -> m
$cfold :: forall m. Monoid m => Type m -> m
Foldable, Functor Type
Foldable Type
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 :: forall (m :: * -> *) a. Monad m => Type (m a) -> m (Type a)
$csequence :: forall (m :: * -> *) a. Monad m => Type (m a) -> m (Type a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type a -> m (Type b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Type a -> m (Type b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Type (f a) -> f (Type a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Type (f a) -> f (Type a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type a -> f (Type b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type a -> f (Type b)
Traversable)

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

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

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

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

srcTypeLevelInt :: Integer -> SourceType
srcTypeLevelInt :: Integer -> Type SourceAnn
srcTypeLevelInt = forall a. a -> Integer -> Type a
TypeLevelInt SourceAnn
NullSourceAnn

srcTypeWildcard :: SourceType
srcTypeWildcard :: Type SourceAnn
srcTypeWildcard = forall a. a -> WildcardData -> Type a
TypeWildcard SourceAnn
NullSourceAnn WildcardData
UnnamedWildcard

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

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

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

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

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

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

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

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

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

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

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

overConstraintArgs :: Functor f => ([Type a] -> f [Type a]) -> Constraint a -> f (Constraint a)
overConstraintArgs :: forall (f :: * -> *) a.
Functor f =>
([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 }) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type a] -> f [Type a]
f (forall a. Constraint a -> [Type a]
constraintArgs Constraint a
c)

mapConstraintArgsAll :: ([Type a] -> [Type a]) -> Constraint a -> Constraint a
mapConstraintArgsAll :: forall a. ([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 (forall a. Constraint a -> [Type a]
constraintKindArgs Constraint a
c)
    , constraintArgs :: [Type a]
constraintArgs = [Type a] -> [Type a]
f (forall a. Constraint a -> [Type a]
constraintArgs Constraint a
c)
    }

overConstraintArgsAll :: Applicative f => ([Type a] -> f [Type a]) -> Constraint a -> f (Constraint a)
overConstraintArgsAll :: forall (f :: * -> *) a.
Applicative f =>
([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 })
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type a] -> f [Type a]
f (forall a. Constraint a -> [Type a]
constraintKindArgs Constraint a
c)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Type a] -> f [Type a]
f (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
    [ Key
"contents" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= ([[Text]]
bs, Bool
trunc)
    ]

constraintToJSON :: (a -> A.Value) -> Constraint a -> A.Value
constraintToJSON :: forall a. (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
    [ Key
"constraintAnn"   forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= a -> Value
annToJSON a
constraintAnn
    , Key
"constraintClass" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= Qualified (ProperName 'ClassName)
constraintClass
    , Key
"constraintKindArgs"  forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. (a -> Value) -> Type a -> Value
typeToJSON a -> Value
annToJSON) [Type a]
constraintKindArgs
    , Key
"constraintArgs"  forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. (a -> Value) -> Type a -> Value
typeToJSON a -> Value
annToJSON) [Type a]
constraintArgs
    , Key
"constraintData"  forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= 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 :: forall a. (a -> Value) -> Type a -> Value
typeToJSON a -> Value
annToJSON Type a
ty =
  case Type a
ty of
    TUnknown a
a Int
b ->
      forall b. ToJSON b => String -> a -> b -> Value
variant String
"TUnknown" a
a Int
b
    TypeVar a
a Text
b ->
      forall b. ToJSON b => String -> a -> b -> Value
variant String
"TypeVar" a
a Text
b
    TypeLevelString a
a PSString
b ->
      forall b. ToJSON b => String -> a -> b -> Value
variant String
"TypeLevelString" a
a PSString
b
    TypeLevelInt a
a Integer
b ->
      forall b. ToJSON b => String -> a -> b -> Value
variant String
"TypeLevelInt" a
a Integer
b
    TypeWildcard a
a WildcardData
b ->
      forall b. ToJSON b => String -> a -> b -> Value
variant String
"TypeWildcard" a
a WildcardData
b
    TypeConstructor a
a Qualified (ProperName 'TypeName)
b ->
      forall b. ToJSON b => String -> a -> b -> Value
variant String
"TypeConstructor" a
a Qualified (ProperName 'TypeName)
b
    TypeOp a
a Qualified (OpName 'TypeOpName)
b ->
      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 ->
      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 ->
      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 -> 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 -> 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 ->
      forall b. ToJSON b => String -> a -> b -> Value
variant String
"ConstrainedType" a
a (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 ->
      forall b. ToJSON b => String -> a -> b -> Value
variant String
"Skolem" a
a (Text
b, Type a -> Value
go 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 ->
      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 ->
      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 ->
      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 ->
      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 = forall a. (a -> Value) -> Type a -> Value
typeToJSON a -> Value
annToJSON

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

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

instance A.ToJSON WildcardData where
  toJSON :: WildcardData -> Value
toJSON = \case
    HoleWildcard Text
name -> Text -> Value
A.String Text
name
    WildcardData
UnnamedWildcard -> Value
A.Null
    WildcardData
IgnoredWildcard -> [Pair] -> Value
A.object [ Key
"ignored" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= Bool
True ]

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

instance A.ToJSON a => A.ToJSON (Constraint a) where
  toJSON :: Constraint a -> Value
toJSON = forall a. (a -> Value) -> Constraint a -> Value
constraintToJSON 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 = forall a. String -> (Object -> Parser a) -> Value -> Parser a
A.withObject String
"PartialConstraintData" forall a b. (a -> b) -> a -> b
$ \Object
o -> do
  ([[Text]]
bs, Bool
trunc) <- Object
o forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"contents"
  forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 :: forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Constraint a)
constraintFromJSON Parser a
defaultAnn Value -> Parser a
annFromJSON = forall a. String -> (Object -> Parser a) -> Value -> Parser a
A.withObject String
"Constraint" forall a b. (a -> b) -> a -> b
$ \Object
o -> do
  a
constraintAnn   <- (Object
o forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"constraintAnn" forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Value -> Parser a
annFromJSON) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser a
defaultAnn
  Qualified (ProperName 'ClassName)
constraintClass <- Object
o forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"constraintClass"
  [Type a]
constraintKindArgs <- Object
o forall a. FromJSON a => Object -> Key -> Parser (Maybe a)
.:? Key
"constraintKindArgs" forall a. Parser (Maybe a) -> a -> Parser a
.!= [] forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
typeFromJSON Parser a
defaultAnn Value -> Parser a
annFromJSON)
  [Type a]
constraintArgs  <- Object
o forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"constraintArgs" forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
typeFromJSON Parser a
defaultAnn Value -> Parser a
annFromJSON)
  Maybe ConstraintData
constraintData  <- Object
o forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"constraintData" forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Value -> Parser ConstraintData
constraintDataFromJSON
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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 :: forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
typeFromJSON Parser a
defaultAnn Value -> Parser a
annFromJSON = forall a. String -> (Object -> Parser a) -> Value -> Parser a
A.withObject String
"Type" forall a b. (a -> b) -> a -> b
$ \Object
o -> do
  String
tag <- Object
o forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"tag"
  a
a   <- (Object
o forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"annotation" forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Value -> Parser a
annFromJSON) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser a
defaultAnn
  let
    contents :: A.FromJSON b => A.Parser b
    contents :: forall b. FromJSON b => Parser b
contents = Object
o forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"contents"
  case String
tag of
    String
"TUnknown" ->
      forall a. a -> Int -> Type a
TUnknown a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b. FromJSON b => Parser b
contents
    String
"TypeVar" ->
      forall a. a -> Text -> Type a
TypeVar a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b. FromJSON b => Parser b
contents
    String
"TypeLevelString" ->
      forall a. a -> PSString -> Type a
TypeLevelString a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b. FromJSON b => Parser b
contents
    String
"TypeLevelInt" ->
      forall a. a -> Integer -> Type a
TypeLevelInt a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b. FromJSON b => Parser b
contents
    String
"TypeWildcard" -> do
      WildcardData
b <- forall b. FromJSON b => Parser b
contents forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a. Applicative f => a -> f a
pure WildcardData
UnnamedWildcard
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> WildcardData -> Type a
TypeWildcard a
a WildcardData
b
    String
"TypeConstructor" ->
      forall a. a -> Qualified (ProperName 'TypeName) -> Type a
TypeConstructor a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b. FromJSON b => Parser b
contents
    String
"TypeOp" ->
      forall a. a -> Qualified (OpName 'TypeOpName) -> Type a
TypeOp a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b. FromJSON b => Parser b
contents
    String
"TypeApp" -> do
      (Value
b, Value
c) <- forall b. FromJSON b => Parser b
contents
      forall a. a -> Type a -> Type a -> Type a
TypeApp a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
b 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) <- forall b. FromJSON b => Parser b
contents
      forall a. a -> Type a -> Type a -> Type a
KindApp a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
b 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) <- forall b. FromJSON b => Parser b
contents
          forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
a Text
b forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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) <- forall b. FromJSON b => Parser b
contents
          forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
a Text
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
c) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser (Type a)
go Value
d forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe SkolemScope
e
      Parser (Type a)
withMbKind forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (Type a)
withoutMbKind
    String
"ConstrainedType" -> do
      (Value
b, Value
c) <- forall b. FromJSON b => Parser b
contents
      forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Constraint a)
constraintFromJSON Parser a
defaultAnn Value -> Parser a
annFromJSON Value
b 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) <- forall b. FromJSON b => Parser b
contents
      Maybe (Type a)
c' <- 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
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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" ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Type a
REmpty a
a
    String
"RCons" -> do
      (Label
b, Value
c, Value
d) <- forall b. FromJSON b => Parser b
contents
      forall a. a -> Label -> Type a -> Type a -> Type a
RCons a
a Label
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
c 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) <- forall b. FromJSON b => Parser b
contents
      forall a. a -> Type a -> Type a -> Type a
KindedType a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
b 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) <- forall b. FromJSON b => Parser b
contents
      forall a. a -> Type a -> Type a -> Type a -> Type a
BinaryNoParensType a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser (Type a)
go Value
c 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 <- forall b. FromJSON b => Parser b
contents
      forall a. a -> Type a -> Type a
ParensInType a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
b
    -- Backwards compatibility for kinds
    String
"KUnknown" ->
      forall a. a -> Int -> Type a
TUnknown a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b. FromJSON b => Parser b
contents
    String
"Row" ->
      forall a. a -> Type a -> Type a -> Type a
TypeApp a
a (forall a. a -> Qualified (ProperName 'TypeName) -> Type a
TypeConstructor a
a Qualified (ProperName 'TypeName)
C.Row) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Parser (Type a)
go forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall b. FromJSON b => Parser b
contents)
    String
"FunKind" -> do
      (Value
b, Value
c) <- forall b. FromJSON b => Parser b
contents
      forall a. a -> Type a -> Type a -> Type a
TypeApp a
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Type a -> Type a -> Type a
TypeApp a
a (forall a. a -> Qualified (ProperName 'TypeName) -> Type a
TypeConstructor a
a Qualified (ProperName 'TypeName)
C.Function) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser (Type a)
go Value
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser (Type a)
go Value
c
    String
"NamedKind" ->
      forall a. a -> Qualified (ProperName 'TypeName) -> Type a
TypeConstructor a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b. FromJSON b => Parser b
contents
    String
other ->
      forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Unrecognised tag: " forall a. [a] -> [a] -> [a]
++ String
other
  where
  go :: A.Value -> A.Parser (Type a)
  go :: Value -> Parser (Type a)
go = 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 (Type SourceAnn)
parseJSON = forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
typeFromJSON (forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceAnn
NullSourceAnn) forall a. FromJSON a => Value -> Parser a
A.parseJSON

instance {-# OVERLAPPING #-} A.FromJSON (Type ()) where
  parseJSON :: Value -> Parser (Type ())
parseJSON = forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
typeFromJSON (forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) 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 = forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Type a)
typeFromJSON (forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Invalid annotation") forall a. FromJSON a => Value -> Parser a
A.parseJSON

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

instance {-# OVERLAPPING #-} A.FromJSON (Constraint ()) where
  parseJSON :: Value -> Parser (Constraint ())
parseJSON = forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Constraint a)
constraintFromJSON (forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) 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 = forall a.
Parser a -> (Value -> Parser a) -> Value -> Parser (Constraint a)
constraintFromJSON (forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Invalid annotation") forall a. FromJSON a => Value -> Parser a
A.parseJSON

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

instance A.FromJSON WildcardData where
  parseJSON :: Value -> Parser WildcardData
parseJSON = \case
    A.String Text
name -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Text -> WildcardData
HoleWildcard Text
name
    A.Object Object
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure WildcardData
IgnoredWildcard
    Value
A.Null -> forall (f :: * -> *) a. Applicative f => a -> f a
pure WildcardData
UnnamedWildcard
    Value
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Unrecognized WildcardData"

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

srcRowListItem :: Label -> SourceType -> RowListItem SourceAnn
srcRowListItem :: Label -> Type SourceAnn -> RowListItem SourceAnn
srcRowListItem = 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 :: forall a. Type a -> ([RowListItem a], Type a)
rowToList = 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) =
    forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall a. a -> Label -> Type a -> RowListItem a
RowListItem a
ann Label
name Type a
ty forall a. a -> [a] -> [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 :: forall a. Type a -> ([RowListItem a], Type a)
rowToSortedList = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall a. RowListItem a -> Label
rowListLabel) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem a]
xs, Type a
r) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(RowListItem a
ann Label
name Type a
ty) -> 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
  :: (Label -> Type a -> Type a -> r)
  -> Type a
  -> Type a
  -> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith :: forall a r.
(Label -> Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith Label -> 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) = forall a. Type a -> ([RowListItem a], Type a)
rowToSortedList Type a
ty1
  ([RowListItem a]
s2, Type a
tail2) = 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) = 
    case forall a. Ord a => a -> a -> Ordering
compare Label
l1 Label
l2 of
      Ordering
LT -> (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first) (forall a. a -> Label -> Type a -> RowListItem a
RowListItem a
a1 Label
l1 Type a
t1 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)
      Ordering
GT -> (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first) (forall a. a -> Label -> Type a -> RowListItem a
RowListItem a
a2 Label
l2 Type a
t2 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)
      Ordering
EQ -> forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (Label -> Type a -> Type a -> r
f Label
l1 Type a
t1 Type a
t2 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 :: forall a. Type a -> Bool
isMonoType ForAll{} = Bool
False
isMonoType (ParensInType a
_ Type a
t) = forall a. Type a -> Bool
isMonoType Type a
t
isMonoType (KindedType a
_ Type a
t Type a
_) = 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 :: forall a. [(a, (Text, Maybe (Type a)))] -> Type a -> Type a
mkForAll [(a, (Text, Maybe (Type a)))]
args Type a
ty = 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 -> 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 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 :: forall a. Text -> Type a -> Type a -> Type a
replaceTypeVars Text
v Type a
r = 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 :: forall a. [(Text, Type a)] -> Type a -> Type a
replaceAllTypeVars = forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [] where
  go :: [Text] -> [(Text, Type a)] -> Type a -> Type a
  go :: forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
_  [(Text, Type a)]
m (TypeVar a
ann Text
v) = forall a. a -> Maybe a -> a
fromMaybe (forall a. a -> Text -> Type a
TypeVar a
ann Text
v) (Text
v 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) = forall a. a -> Type a -> Type a -> Type a
TypeApp a
ann (forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t1) (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) = forall a. a -> Type a -> Type a -> Type a
KindApp a
ann (forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t1) (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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
keys = forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs (forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
/= Text
v) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Text, Type a)]
m) forall a b. (a -> b) -> a -> b
$ 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
usedVars =
      let v' :: Text
v' = forall {t :: * -> *}. Foldable t => Text -> t Text -> Text
genName Text
v ([Text]
keys forall a. [a] -> [a] -> [a]
++ [Text]
bs forall a. [a] -> [a] -> [a]
++ [Text]
usedVars)
          t' :: Type a
t' = forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text
v, forall a. a -> Text -> Type a
TypeVar a
ann Text
v')] Type a
t
      in forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
v' Maybe (Type a)
mbK' (forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go (Text
v' forall a. a -> [a] -> [a]
: [Text]
bs) [(Text, Type a)]
m Type a
t') Maybe SkolemScope
sco
    | Bool
otherwise = forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
v Maybe (Type a)
mbK' (forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go (Text
v forall a. a -> [a] -> [a]
: [Text]
bs) [(Text, Type a)]
m Type a
t) Maybe SkolemScope
sco
    where
      mbK' :: Maybe (Type a)
mbK' = forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Type a)
mbK
      keys :: [Text]
keys = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Text, Type a)]
m
      usedVars :: [Text]
usedVars = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a. Type a -> [Text]
usedTypeVariables forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
ann (forall a. ([Type a] -> [Type a]) -> Constraint a -> Constraint a
mapConstraintArgsAll (forall a b. (a -> b) -> [a] -> [b]
map (forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m)) Constraint a
c) (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) = forall a. a -> Label -> Type a -> Type a -> Type a
RCons a
ann Label
name' (forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t) (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) = forall a. a -> Type a -> Type a -> Type a
KindedType a
ann (forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t) (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) = forall a. a -> Type a -> Type a -> Type a -> Type a
BinaryNoParensType a
ann (forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t1) (forall a. [Text] -> [(Text, Type a)] -> Type a -> Type a
go [Text]
bs [(Text, Type a)]
m Type a
t2) (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) = forall a. a -> Type a -> Type a
ParensInType a
ann (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 forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (forall a. Show a => a -> String
show Integer
n)) forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Text
inUse = Integer -> Text
try' (Integer
n forall a. Num a => a -> a -> a
+ Integer
1)
           | Bool
otherwise = Text
orig forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (forall a. Show a => a -> String
show Integer
n)

-- | Collect all type variables appearing in a type
usedTypeVariables :: Type a -> [Text]
usedTypeVariables :: forall a. Type a -> [Text]
usedTypeVariables = forall a. Ord a => [a] -> [a]
ordNub forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes forall a. [a] -> [a] -> [a]
(++) 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 :: forall a. Type a -> [Text]
freeTypeVariables = forall a. Ord a => [a] -> [a]
ordNub forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound (TypeVar a
_ Text
v) | Text
v 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) = forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t1 forall a. [a] -> [a] -> [a]
++ 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) = forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t1 forall a. [a] -> [a] -> [a]
++ forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go (Int
lvl 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
_) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go (Int
lvl forall a. Num a => a -> a -> a
- Int
1) [Text]
bound) Maybe (Type a)
mbK forall a. [a] -> [a] -> [a]
++ forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl (Text
v forall a. a -> [a] -> [a]
: [Text]
bound) Type a
t
  go Int
lvl [Text]
bound (ConstrainedType a
_ Constraint a
c Type a
t) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go (Int
lvl forall a. Num a => a -> a -> a
- Int
1) [Text]
bound) (forall a. Constraint a -> [Type a]
constraintKindArgs Constraint a
c) forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound) (forall a. Constraint a -> [Type a]
constraintArgs Constraint a
c) forall a. [a] -> [a] -> [a]
++ 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) = forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t forall a. [a] -> [a] -> [a]
++ 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) = forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t forall a. [a] -> [a] -> [a]
++ forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go (Int
lvl 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) = forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t1 forall a. [a] -> [a] -> [a]
++ forall a. Int -> [Text] -> Type a -> [(Int, Text)]
go Int
lvl [Text]
bound Type a
t2 forall a. [a] -> [a] -> [a]
++ 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) = 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 :: forall a. Type a -> Maybe ([(a, (Text, Type a))], Type a)
completeBinderList = 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
_ -> 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)) forall a. a -> [a] -> [a]
: [(a, (Text, Type a))]
acc) Type a
ty
    Type a
ty -> forall a. a -> Maybe a
Just (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 :: forall a. Type a -> Type a
quantify Type a
ty = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Text
arg Type a
t -> forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll (forall a. Type a -> a
getAnnForType Type a
ty) Text
arg forall a. Maybe a
Nothing Type a
t forall a. Maybe a
Nothing) Type a
ty forall a b. (a -> b) -> a -> b
$ 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 :: forall a. Type a -> Type a
moveQuantifiersToFront = 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) 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) 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 = 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) -> 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) (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Type a
ty' (a
ann, Constraint a
c) -> 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 `forall`
containsForAll :: Type a -> Bool
containsForAll :: forall a. Type a -> Bool
containsForAll = forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes Bool -> Bool -> Bool
(||) forall a. Type a -> Bool
go where
  go :: Type a -> Bool
  go :: forall a. Type a -> Bool
go ForAll{} = Bool
True
  go Type a
_ = Bool
False

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

-- | Check if a type contains unknowns in a position that is relevant to
-- constraint solving. (Kinds are not.)
containsUnknowns :: Type a -> Bool
containsUnknowns :: forall a. Type a -> Bool
containsUnknowns = forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes Bool -> Bool -> Bool
(||) forall a. Type a -> Bool
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> Type a
eraseKindApps where
  go :: Type a -> Bool
  go :: forall a. Type a -> Bool
go TUnknown{} = Bool
True
  go Type a
_ = Bool
False

eraseKindApps :: Type a -> Type a
eraseKindApps :: forall a. Type a -> Type a
eraseKindApps = forall a. (Type a -> Type a) -> Type a -> Type a
everywhereOnTypes 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 ->
    forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
ann (Constraint a
con { constraintKindArgs :: [Type a]
constraintKindArgs = [] }) Type a
ty
  Skolem a
ann Text
name Maybe (Type a)
_ Int
i SkolemScope
sc ->
    forall a.
a -> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a
Skolem a
ann Text
name forall a. Maybe a
Nothing Int
i SkolemScope
sc
  Type a
other -> Type a
other

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

  removeAmbiguousVars :: Type a -> Type a
removeAmbiguousVars = forall a. (Type a -> Type a) -> Type a -> Type a
everywhereOnTypes 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` 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 :: forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes = 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 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) = 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 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 :: forall a. Type a -> ([Constraint a], Type a)
unapplyConstraints = 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 forall a. a -> [a] -> [a]
: [Constraint a]
acc) Type a
ty
  go [Constraint a]
acc Type a
ty = (forall a. [a] -> [a]
reverse [Constraint a]
acc, Type a
ty)

-- | Construct the type of an instance declaration from its parts. Used in
-- error messages describing unnamed instances.
srcInstanceType
  :: SourceSpan
  -> [(Text, SourceType)]
  -> Qualified (ProperName 'ClassName)
  -> [SourceType]
  -> SourceType
srcInstanceType :: SourceSpan
-> [(Text, Type SourceAnn)]
-> Qualified (ProperName 'ClassName)
-> [Type SourceAnn]
-> Type SourceAnn
srcInstanceType SourceSpan
ss [(Text, Type SourceAnn)]
vars Qualified (ProperName 'ClassName)
className [Type SourceAnn]
tys
  = forall a. a -> Type a -> Type a
setAnnForType (SourceSpan
ss, [])
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a b. (a -> b) -> a -> b
$ \(Text
tv, Type SourceAnn
k) Type SourceAnn
ty -> Text
-> Maybe (Type SourceAnn)
-> Type SourceAnn
-> Maybe SkolemScope
-> Type SourceAnn
srcForAll Text
tv (forall a. a -> Maybe a
Just Type SourceAnn
k) Type SourceAnn
ty forall a. Maybe a
Nothing) [(Text, Type SourceAnn)]
vars
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type SourceAnn -> Type SourceAnn -> Type SourceAnn
srcTypeApp) [Type SourceAnn]
tys
  forall a b. (a -> b) -> a -> b
$ Qualified (ProperName 'TypeName) -> Type SourceAnn
srcTypeConstructor forall a b. (a -> b) -> a -> b
$ forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a -> ProperName b
coerceProperName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualified (ProperName 'ClassName)
className

everywhereOnTypes :: (Type a -> Type a) -> Type a -> Type a
everywhereOnTypes :: forall a. (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 (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 (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 (forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
arg (Type a -> Type a
go 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 (forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
ann (forall a. ([Type a] -> [Type a]) -> Constraint a -> Constraint a
mapConstraintArgsAll (forall a b. (a -> b) -> [a] -> [b]
map Type a -> Type a
go) Constraint a
c) (Type a -> Type a
go Type a
ty))
  go (Skolem a
ann Text
name Maybe (Type a)
mbK Int
i SkolemScope
sc) = Type a -> Type a
f (forall a.
a -> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a
Skolem a
ann Text
name (Type a -> Type a
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Type a)
mbK) Int
i SkolemScope
sc)
  go (RCons a
ann Label
name Type a
ty Type a
rest) = Type a -> Type a
f (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 (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 (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 (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

everywhereOnTypesM :: Monad m => (Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereOnTypesM :: forall (m :: * -> *) a.
Monad m =>
(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) = (forall a. a -> Type a -> Type a -> Type a
TypeApp a
ann forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type a -> m (Type a)
go Type a
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
t2) 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) = (forall a. a -> Type a -> Type a -> Type a
KindApp a
ann forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type a -> m (Type a)
go Type a
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
t2) 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) = (forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
arg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
ty forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe SkolemScope
sco) 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) = (forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
ann forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a.
Applicative f =>
([Type a] -> f [Type a]) -> Constraint a -> f (Constraint a)
overConstraintArgsAll (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 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
ty) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type a -> m (Type a)
f
  go (Skolem a
ann Text
name Maybe (Type a)
mbK Int
i SkolemScope
sc) = (forall a.
a -> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a
Skolem a
ann Text
name forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
i forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SkolemScope
sc) 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) = (forall a. a -> Label -> Type a -> Type a -> Type a
RCons a
ann Label
name forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type a -> m (Type a)
go Type a
ty forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
rest) 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) = (forall a. a -> Type a -> Type a -> Type a
KindedType a
ann forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type a -> m (Type a)
go Type a
ty forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
k) 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) = (forall a. a -> Type a -> Type a -> Type a -> Type a
BinaryNoParensType a
ann forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type a -> m (Type a)
go Type a
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
t2 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type a -> m (Type a)
go Type a
t3) 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) = (forall a. a -> Type a -> Type a
ParensInType a
ann forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type a -> m (Type a)
go Type a
t) 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

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

everythingOnTypes :: (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes :: forall r a. (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) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl r -> r -> r
(<+>) (Type a -> r
f Type a
t) (forall a b. (a -> b) -> [a] -> [b]
map Type a -> r
go (forall a. Constraint a -> [Type a]
constraintKindArgs Constraint a
c) forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map Type a -> r
go (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@(Skolem a
_ Text
_ (Just Type a
k) Int
_ SkolemScope
_) = Type a -> r
f Type a
t r -> r -> r
<+> Type a -> r
go Type a
k
  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 :: forall s r a.
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) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl r -> r -> r
(<+>) r
r0 (forall a b. (a -> b) -> [a] -> [b]
map (s -> Type a -> r
go' s
s) (forall a. Constraint a -> [Type a]
constraintKindArgs Constraint a
c) forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (s -> Type a -> r
go' s
s) (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 (Skolem a
_ Text
_ (Just Type a
k) Int
_ SkolemScope
_) = s -> Type a -> r
go' s
s Type a
k
  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 :: forall a. Lens' (Type a) a
annForType a -> f a
k (TUnknown a
a Int
b) = (\a
z -> forall a. a -> Int -> Type a
TUnknown a
z Int
b) 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 -> forall a. a -> Text -> Type a
TypeVar a
z Text
b) 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 -> forall a. a -> PSString -> Type a
TypeLevelString a
z PSString
b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a
annForType a -> f a
k (TypeLevelInt a
a Integer
b) = (\a
z -> forall a. a -> Integer -> Type a
TypeLevelInt a
z Integer
b) 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 WildcardData
b) = (\a
z -> forall a. a -> WildcardData -> Type a
TypeWildcard a
z WildcardData
b) 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 -> forall a. a -> Qualified (ProperName 'TypeName) -> Type a
TypeConstructor a
z Qualified (ProperName 'TypeName)
b) 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 -> forall a. a -> Qualified (OpName 'TypeOpName) -> Type a
TypeOp a
z Qualified (OpName 'TypeOpName)
b) 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 -> forall a. a -> Type a -> Type a -> Type a
TypeApp a
z Type a
b Type a
c) 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 -> forall a. a -> Type a -> Type a -> Type a
KindApp a
z Type a
b Type a
c) 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 -> 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) 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 -> forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType a
z Constraint a
b Type a
c) 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 -> forall a.
a -> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a
Skolem a
z Text
b Maybe (Type a)
c Int
d SkolemScope
e) 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) = forall a. a -> Type a
REmpty 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 -> forall a. a -> Label -> Type a -> Type a -> Type a
RCons a
z Label
b Type a
c Type a
d) 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 -> forall a. a -> Type a -> Type a -> Type a
KindedType a
z Type a
b Type a
c) 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 -> forall a. a -> Type a -> Type a -> Type a -> Type a
BinaryNoParensType a
z Type a
b Type a
c Type a
d) 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 -> forall a. a -> Type a -> Type a
ParensInType a
z Type a
b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
k a
a

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

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

instance Eq (Type a) where
  == :: 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 = forall a b. Type a -> Type b -> Ordering
compareType

eqType :: Type a -> Type b -> Bool
eqType :: forall a b. Type a -> Type b -> Bool
eqType (TUnknown a
_ Int
a) (TUnknown b
_ Int
a') = Int
a forall a. Eq a => a -> a -> Bool
== Int
a'
eqType (TypeVar a
_ Text
a) (TypeVar b
_ Text
a') = Text
a forall a. Eq a => a -> a -> Bool
== Text
a'
eqType (TypeLevelString a
_ PSString
a) (TypeLevelString b
_ PSString
a') = PSString
a forall a. Eq a => a -> a -> Bool
== PSString
a'
eqType (TypeLevelInt a
_ Integer
a) (TypeLevelInt b
_ Integer
a') = Integer
a forall a. Eq a => a -> a -> Bool
== Integer
a'
eqType (TypeWildcard a
_ WildcardData
a) (TypeWildcard b
_ WildcardData
a') = WildcardData
a forall a. Eq a => a -> a -> Bool
== WildcardData
a'
eqType (TypeConstructor a
_ Qualified (ProperName 'TypeName)
a) (TypeConstructor b
_ Qualified (ProperName 'TypeName)
a') = Qualified (ProperName 'TypeName)
a 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 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') = forall a b. Type a -> Type b -> Bool
eqType Type a
a Type b
a' Bool -> Bool -> 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') = forall a b. Type a -> Type b -> Bool
eqType Type a
a Type b
a' Bool -> Bool -> 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 forall a. Eq a => a -> a -> Bool
== Text
a' Bool -> Bool -> Bool
&& forall a b. Maybe (Type a) -> Maybe (Type b) -> Bool
eqMaybeType Maybe (Type a)
b Maybe (Type b)
b' Bool -> Bool -> Bool
&& forall a b. Type a -> Type b -> Bool
eqType Type a
c Type b
c' Bool -> Bool -> Bool
&& Maybe SkolemScope
d 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') = forall a b. Constraint a -> Constraint b -> Bool
eqConstraint Constraint a
a Constraint b
a' Bool -> Bool -> 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 forall a. Eq a => a -> a -> Bool
== Text
a' Bool -> Bool -> 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 forall a. Eq a => a -> a -> Bool
== Int
c' Bool -> Bool -> Bool
&& SkolemScope
d 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 forall a. Eq a => a -> a -> Bool
== Label
a' Bool -> Bool -> Bool
&& forall a b. Type a -> Type b -> Bool
eqType Type a
b Type b
b' Bool -> Bool -> 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') = forall a b. Type a -> Type b -> Bool
eqType Type a
a Type b
a' Bool -> Bool -> 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') = forall a b. Type a -> Type b -> Bool
eqType Type a
a Type b
a' Bool -> Bool -> Bool
&& forall a b. Type a -> Type b -> Bool
eqType Type a
b Type b
b' Bool -> Bool -> 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') = 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 :: forall a b. Maybe (Type a) -> Maybe (Type b) -> Bool
eqMaybeType (Just Type a
a) (Just Type b
b) = 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 :: forall a b. Type a -> Type b -> Ordering
compareType (TUnknown a
_ Int
a) (TUnknown b
_ Int
a') = forall a. Ord a => a -> a -> Ordering
compare Int
a Int
a'
compareType (TypeVar a
_ Text
a) (TypeVar b
_ Text
a') = forall a. Ord a => a -> a -> Ordering
compare Text
a Text
a'
compareType (TypeLevelString a
_ PSString
a) (TypeLevelString b
_ PSString
a') = forall a. Ord a => a -> a -> Ordering
compare PSString
a PSString
a'
compareType (TypeLevelInt a
_ Integer
a) (TypeLevelInt b
_ Integer
a') = forall a. Ord a => a -> a -> Ordering
compare Integer
a Integer
a'
compareType (TypeWildcard a
_ WildcardData
a) (TypeWildcard b
_ WildcardData
a') = forall a. Ord a => a -> a -> Ordering
compare WildcardData
a WildcardData
a'
compareType (TypeConstructor a
_ Qualified (ProperName 'TypeName)
a) (TypeConstructor b
_ Qualified (ProperName 'TypeName)
a') = 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') = 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') = forall a b. Type a -> Type b -> Ordering
compareType Type a
a Type b
a' forall a. Semigroup a => a -> a -> a
<> 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') = forall a b. Type a -> Type b -> Ordering
compareType Type a
a Type b
a' forall a. Semigroup a => a -> a -> a
<> 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') = forall a. Ord a => a -> a -> Ordering
compare Text
a Text
a' forall a. Semigroup a => a -> a -> a
<> forall a b. Maybe (Type a) -> Maybe (Type b) -> Ordering
compareMaybeType Maybe (Type a)
b Maybe (Type b)
b' forall a. Semigroup a => a -> a -> a
<> forall a b. Type a -> Type b -> Ordering
compareType Type a
c Type b
c' forall a. Semigroup a => a -> a -> a
<> 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') = forall a b. Constraint a -> Constraint b -> Ordering
compareConstraint Constraint a
a Constraint b
a' forall a. Semigroup a => a -> a -> a
<> 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') = forall a. Ord a => a -> a -> Ordering
compare Text
a Text
a' forall a. Semigroup a => a -> a -> a
<> forall a b. Maybe (Type a) -> Maybe (Type b) -> Ordering
compareMaybeType Maybe (Type a)
b Maybe (Type b)
b' forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => a -> a -> Ordering
compare Int
c Int
c' forall a. Semigroup a => a -> a -> a
<> 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') = forall a. Ord a => a -> a -> Ordering
compare Label
a Label
a' forall a. Semigroup a => a -> a -> a
<> forall a b. Type a -> Type b -> Ordering
compareType Type a
b Type b
b' forall a. Semigroup a => a -> a -> a
<> 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') = forall a b. Type a -> Type b -> Ordering
compareType Type a
a Type b
a' forall a. Semigroup a => a -> a -> a
<> 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') = forall a b. Type a -> Type b -> Ordering
compareType Type a
a Type b
a' forall a. Semigroup a => a -> a -> a
<> forall a b. Type a -> Type b -> Ordering
compareType Type a
b Type b
b' forall a. Semigroup a => a -> a -> a
<> 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') = forall a b. Type a -> Type b -> Ordering
compareType Type a
a Type b
a'
compareType Type a
typ Type b
typ' =
  forall a. Ord a => a -> a -> Ordering
compare (forall a. Type a -> Int
orderOf Type a
typ) (forall a. Type a -> Int
orderOf Type b
typ')
    where
      orderOf :: Type a -> Int
      orderOf :: forall a. Type a -> Int
orderOf TUnknown{} = Int
0
      orderOf TypeVar{} = Int
1
      orderOf TypeLevelString{} = Int
2
      orderOf TypeLevelInt{} = Int
3
      orderOf TypeWildcard{} = Int
4
      orderOf TypeConstructor{} = Int
5
      orderOf TypeOp{} = Int
6
      orderOf TypeApp{} = Int
7
      orderOf KindApp{} = Int
8
      orderOf ForAll{} = Int
9
      orderOf ConstrainedType{} = Int
10
      orderOf Skolem{} = Int
11
      orderOf REmpty{} = Int
12
      orderOf RCons{} = Int
13
      orderOf KindedType{} = Int
14
      orderOf BinaryNoParensType{} = Int
15
      orderOf ParensInType{} = Int
16

compareMaybeType :: Maybe (Type a) -> Maybe (Type b) -> Ordering
compareMaybeType :: forall a b. Maybe (Type a) -> Maybe (Type b) -> Ordering
compareMaybeType (Just Type a
a) (Just Type b
b) = 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
(==) = forall a b. Constraint a -> Constraint b -> Bool
eqConstraint

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

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

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