module Language.PureScript.TypeChecker.Kinds
( kindOf
, kindOfWithUnknowns
, kindOfWithScopedVars
, kindOfData
, kindOfTypeSynonym
, kindOfClass
, kindsOfAll
, unifyKinds
, unifyKinds'
, subsumesKind
, instantiateKind
, checkKind
, inferKind
, elaborateKind
, checkConstraint
, checkInstanceDeclaration
, checkKindDeclaration
, checkTypeKind
, unknownsWithKinds
, freshKind
, freshKindWithKind
) where
import Prelude
import Control.Arrow ((***))
import Control.Lens ((^.), _1, _2, _3)
import Control.Monad (join, unless, void, when, (<=<))
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State (MonadState, gets, modify)
import Control.Monad.Supply.Class (MonadSupply(..))
import Data.Bifunctor (first, second)
import Data.Bitraversable (bitraverse)
import Data.Foldable (for_, traverse_)
import Data.Function (on)
import Data.Functor (($>))
import Data.IntSet qualified as IS
import Data.List (nubBy, sortOn, (\\))
import Data.Map qualified as M
import Data.Maybe (fromJust, fromMaybe)
import Data.Text (Text)
import Data.Text qualified as T
import Data.Traversable (for)
import Language.PureScript.Crash (HasCallStack, internalError)
import Language.PureScript.Environment qualified as E
import Language.PureScript.Errors
import Language.PureScript.Names (pattern ByNullSourcePos, ModuleName, Name(..), ProperName(..), ProperNameType(..), Qualified(..), QualifiedBy(..), coerceProperName, mkQualified)
import Language.PureScript.TypeChecker.Monad (CheckState(..), Substitution(..), UnkLevel(..), Unknown, bindLocalTypeVariables, debugType, getEnv, lookupTypeVariable, unsafeCheckCurrentModule, withErrorMessageHint, withFreshSubstitution)
import Language.PureScript.TypeChecker.Skolems (newSkolemConstant, newSkolemScope, skolemize)
import Language.PureScript.TypeChecker.Synonyms (replaceAllTypeSynonyms)
import Language.PureScript.Types
import Language.PureScript.Pretty.Types (prettyPrintType)
generalizeUnknowns :: [(Unknown, SourceType)] -> SourceType -> SourceType
generalizeUnknowns :: [(Int, SourceType)] -> SourceType -> SourceType
generalizeUnknowns [(Int, SourceType)]
unks SourceType
ty =
[(Int, (Text, SourceType))] -> SourceType -> SourceType
generalizeUnknownsWithVars ([Text] -> [(Int, SourceType)] -> [(Int, (Text, SourceType))]
unknownVarNames (forall a. Type a -> [Text]
usedTypeVariables SourceType
ty) [(Int, SourceType)]
unks) SourceType
ty
generalizeUnknownsWithVars :: [(Unknown, (Text, SourceType))] -> SourceType -> SourceType
generalizeUnknownsWithVars :: [(Int, (Text, SourceType))] -> SourceType -> SourceType
generalizeUnknownsWithVars [(Int, (Text, SourceType))]
binders SourceType
ty =
forall a. [(a, (Text, Maybe (Type a)))] -> Type a -> Type a
mkForAll ((forall a. Type a -> a
getAnnForType SourceType
ty,) 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. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [(Int, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars [(Int, (Text, SourceType))]
binders) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, (Text, SourceType))]
binders) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [(Int, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars [(Int, (Text, SourceType))]
binders forall a b. (a -> b) -> a -> b
$ SourceType
ty
replaceUnknownsWithVars :: [(Unknown, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars :: forall a. [(Int, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars [(Int, (Text, a))]
binders SourceType
ty
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, (Text, a))]
binders = SourceType
ty
| Bool
otherwise = SourceType -> SourceType
go SourceType
ty
where
go :: SourceType -> SourceType
go :: SourceType -> SourceType
go = forall a. (Type a -> Type a) -> Type a -> Type a
everywhereOnTypes forall a b. (a -> b) -> a -> b
$ \case
TUnknown SourceAnn
ann Int
unk | Just (Text
name, a
_) <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
unk [(Int, (Text, a))]
binders -> forall a. a -> Text -> Type a
TypeVar SourceAnn
ann Text
name
SourceType
other -> SourceType
other
unknownVarNames :: [Text] -> [(Unknown, SourceType)] -> [(Unknown, (Text, SourceType))]
unknownVarNames :: [Text] -> [(Int, SourceType)] -> [(Int, (Text, SourceType))]
unknownVarNames [Text]
used [(Int, SourceType)]
unks =
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Int
a, SourceType
b) Text
n -> (Int
a, (Text
n, SourceType
b))) [(Int, SourceType)]
unks forall a b. (a -> b) -> a -> b
$ [Text]
allVars forall a. Eq a => [a] -> [a] -> [a]
\\ [Text]
used
where
allVars :: [Text]
allVars :: [Text]
allVars
| [(Int, SourceType)
_] <- [(Int, SourceType)]
unks = Text
"k" forall a. a -> [a] -> [a]
: [Text]
vars
| Bool
otherwise = [Text]
vars
vars :: [Text]
vars :: [Text]
vars = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Text
"k" forall a. Semigroup a => a -> a -> a
<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) ([Int
1..] :: [Int])
apply :: (MonadState CheckState m) => SourceType -> m SourceType
apply :: forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
ty = forall a b c. (a -> b -> c) -> b -> a -> c
flip Substitution -> SourceType -> SourceType
substituteType SourceType
ty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Substitution
checkSubstitution
substituteType :: Substitution -> SourceType -> SourceType
substituteType :: Substitution -> SourceType -> SourceType
substituteType Substitution
sub = forall a. (Type a -> Type a) -> Type a -> Type a
everywhereOnTypes forall a b. (a -> b) -> a -> b
$ \case
TUnknown SourceAnn
ann Int
u ->
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
u (Substitution -> Map Int SourceType
substType Substitution
sub) of
Maybe SourceType
Nothing -> forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u
Just (TUnknown SourceAnn
ann' Int
u1) | Int
u1 forall a. Eq a => a -> a -> Bool
== Int
u -> forall a. a -> Int -> Type a
TUnknown SourceAnn
ann' Int
u1
Just SourceType
t -> Substitution -> SourceType -> SourceType
substituteType Substitution
sub SourceType
t
SourceType
other ->
SourceType
other
freshUnknown :: (MonadState CheckState m) => m Unknown
freshUnknown :: forall (m :: * -> *). MonadState CheckState m => m Int
freshUnknown = do
Int
k <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Int
checkNextType
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CheckState
st -> CheckState
st { checkNextType :: Int
checkNextType = Int
k forall a. Num a => a -> a -> a
+ Int
1 }
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
k
freshKind :: (MonadState CheckState m) => SourceSpan -> m SourceType
freshKind :: forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind SourceSpan
ss = forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> SourceType -> m SourceType
freshKindWithKind SourceSpan
ss SourceType
E.kindType
freshKindWithKind :: (MonadState CheckState m) => SourceSpan -> SourceType -> m SourceType
freshKindWithKind :: forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> SourceType -> m SourceType
freshKindWithKind SourceSpan
ss SourceType
kind = do
Int
u <- forall (m :: * -> *). MonadState CheckState m => m Int
freshUnknown
forall (m :: * -> *).
MonadState CheckState m =>
Maybe UnkLevel -> Int -> SourceType -> m ()
addUnsolved forall a. Maybe a
Nothing Int
u SourceType
kind
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Int -> Type a
TUnknown (SourceSpan
ss, []) Int
u
addUnsolved :: (MonadState CheckState m) => Maybe UnkLevel -> Unknown -> SourceType -> m ()
addUnsolved :: forall (m :: * -> *).
MonadState CheckState m =>
Maybe UnkLevel -> Int -> SourceType -> m ()
addUnsolved Maybe UnkLevel
lvl Int
unk SourceType
kind = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CheckState
st -> do
let
newLvl :: UnkLevel
newLvl = NonEmpty Int -> UnkLevel
UnkLevel forall a b. (a -> b) -> a -> b
$ case Maybe UnkLevel
lvl of
Maybe UnkLevel
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
unk
Just (UnkLevel NonEmpty Int
lvl') -> NonEmpty Int
lvl' forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
unk
subs :: Substitution
subs = CheckState -> Substitution
checkSubstitution CheckState
st
uns :: Map Int (UnkLevel, SourceType)
uns = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
unk (UnkLevel
newLvl, SourceType
kind) forall a b. (a -> b) -> a -> b
$ Substitution -> Map Int (UnkLevel, SourceType)
substUnsolved Substitution
subs
CheckState
st { checkSubstitution :: Substitution
checkSubstitution = Substitution
subs { substUnsolved :: Map Int (UnkLevel, SourceType)
substUnsolved = Map Int (UnkLevel, SourceType)
uns } }
solve :: (MonadState CheckState m) => Unknown -> SourceType -> m ()
solve :: forall (m :: * -> *).
MonadState CheckState m =>
Int -> SourceType -> m ()
solve Int
unk SourceType
solution = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CheckState
st -> do
let
subs :: Substitution
subs = CheckState -> Substitution
checkSubstitution CheckState
st
tys :: Map Int SourceType
tys = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
unk SourceType
solution forall a b. (a -> b) -> a -> b
$ Substitution -> Map Int SourceType
substType Substitution
subs
CheckState
st { checkSubstitution :: Substitution
checkSubstitution = Substitution
subs { substType :: Map Int SourceType
substType = Map Int SourceType
tys } }
lookupUnsolved
:: (MonadState CheckState m, MonadError MultipleErrors m, HasCallStack)
=> Unknown
-> m (UnkLevel, SourceType)
lookupUnsolved :: forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
u = do
Map Int (UnkLevel, SourceType)
uns <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Substitution -> Map Int (UnkLevel, SourceType)
substUnsolved forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckState -> Substitution
checkSubstitution)
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
u Map Int (UnkLevel, SourceType)
uns of
Maybe (UnkLevel, SourceType)
Nothing -> forall (m :: * -> *) a.
(MonadError MultipleErrors m, HasCallStack) =>
Text -> m a
internalCompilerError forall a b. (a -> b) -> a -> b
$ Text
"Unsolved unification variable ?" forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (forall a. Show a => a -> String
show Int
u) forall a. Semigroup a => a -> a -> a
<> Text
" is not bound"
Just (UnkLevel, SourceType)
res -> forall (m :: * -> *) a. Monad m => a -> m a
return (UnkLevel, SourceType)
res
unknownsWithKinds
:: forall m. (MonadState CheckState m, MonadError MultipleErrors m, HasCallStack)
=> [Unknown]
-> m [(Unknown, SourceType)]
unknownsWithKinds :: forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
[Int] -> m [(Int, SourceType)]
unknownsWithKinds = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 a. (a -> a -> Bool) -> [a] -> [a]
nubBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst) 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 (m :: * -> *) a. Monad m => m (m a) -> m a
join) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall {m :: * -> *}.
(MonadState CheckState m, MonadError MultipleErrors m) =>
Int -> m [(UnkLevel, (Int, SourceType))]
go
where
go :: Int -> m [(UnkLevel, (Int, SourceType))]
go Int
u = do
(UnkLevel
lvl, SourceType
ty) <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
u
[(UnkLevel, (Int, SourceType))]
rest <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Int -> m [(UnkLevel, (Int, SourceType))]
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IS.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> IntSet
unknowns forall a b. (a -> b) -> a -> b
$ SourceType
ty
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (UnkLevel
lvl, (Int
u, SourceType
ty)) forall a. a -> [a] -> [a]
: [(UnkLevel, (Int, SourceType))]
rest
inferKind
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceType
-> m (SourceType, SourceType)
inferKind :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (SourceType, SourceType)
inferKind = \SourceType
tyToInfer ->
forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint (SourceType -> ErrorMessageHint
ErrorInferringKind SourceType
tyToInfer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
MonadError MultipleErrors m =>
SourceSpan -> m a -> m a
rethrowWithPosition (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. Type a -> a
getAnnForType SourceType
tyToInfer)
forall a b. (a -> b) -> a -> b
$ SourceType -> m (SourceType, SourceType)
go SourceType
tyToInfer
where
go :: SourceType -> m (SourceType, SourceType)
go = \case
ty :: SourceType
ty@(TypeConstructor SourceAnn
ann Qualified (ProperName 'TypeName)
v) -> do
Environment
env <- forall (m :: * -> *). MonadState CheckState m => m Environment
getEnv
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'TypeName)
v (Environment
-> Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
E.types Environment
env) of
Maybe (SourceType, TypeKind)
Nothing ->
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' (forall a b. (a, b) -> a
fst SourceAnn
ann) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Qualified Name -> SimpleErrorMessage
UnknownName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProperName 'TypeName -> Name
TyName forall a b. (a -> b) -> a -> b
$ Qualified (ProperName 'TypeName)
v
Just (SourceType
kind, TypeKind
E.LocalTypeVariable) -> do
SourceType
kind' <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
kind
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
kind' forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
Just (SourceType
kind, TypeKind
_) -> do
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
kind forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
ConstrainedType SourceAnn
ann' con :: Constraint SourceAnn
con@(Constraint SourceAnn
ann Qualified (ProperName 'ClassName)
v [SourceType]
_ [SourceType]
_ Maybe ConstraintData
_) SourceType
ty -> do
Environment
env <- forall (m :: * -> *). MonadState CheckState m => m Environment
getEnv
Constraint SourceAnn
con' <- case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (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)
v) (Environment
-> Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
E.types Environment
env) of
Maybe (SourceType, TypeKind)
Nothing ->
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' (forall a b. (a, b) -> a
fst SourceAnn
ann) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Qualified Name -> SimpleErrorMessage
UnknownName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProperName 'ClassName -> Name
TyClassName forall a b. (a -> b) -> a -> b
$ Qualified (ProperName 'ClassName)
v
Just (SourceType, TypeKind)
_ ->
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Constraint SourceAnn -> m (Constraint SourceAnn)
checkConstraint Constraint SourceAnn
con
SourceType
ty' <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
checkIsSaturatedType SourceType
ty
Constraint SourceAnn
con'' <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Constraint SourceAnn -> m (Constraint SourceAnn)
applyConstraint Constraint SourceAnn
con'
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType SourceAnn
ann' Constraint SourceAnn
con'' SourceType
ty', SourceType
E.kindType forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann')
ty :: SourceType
ty@(TypeLevelString SourceAnn
ann PSString
_) ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
E.kindSymbol forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
ty :: SourceType
ty@(TypeLevelInt SourceAnn
ann Integer
_) ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
E.tyInt forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
ty :: SourceType
ty@(TypeVar SourceAnn
ann Text
v) -> do
ModuleName
moduleName <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
m ModuleName
unsafeCheckCurrentModule
SourceType
kind <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
ModuleName -> Qualified (ProperName 'TypeName) -> m SourceType
lookupTypeVariable ModuleName
moduleName (forall a. QualifiedBy -> a -> Qualified a
Qualified QualifiedBy
ByNullSourcePos forall a b. (a -> b) -> a -> b
$ forall (a :: ProperNameType). Text -> ProperName a
ProperName Text
v)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
kind forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
ty :: SourceType
ty@(Skolem SourceAnn
ann Text
_ Maybe SourceType
mbK Int
_ SkolemScope
_) -> do
SourceType
kind <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
internalError String
"Skolem has no kind") Maybe SourceType
mbK
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
kind forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
ty :: SourceType
ty@(TUnknown SourceAnn
ann Int
u) -> do
SourceType
kind <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
u
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
kind forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
ty :: SourceType
ty@(TypeWildcard SourceAnn
ann WildcardData
_) -> do
SourceType
k <- forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind (forall a b. (a, b) -> a
fst SourceAnn
ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
k forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
ty :: SourceType
ty@(REmpty SourceAnn
ann) -> do
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
E.kindOfREmpty forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
ty :: SourceType
ty@(RCons SourceAnn
ann Label
_ SourceType
_ SourceType
_) | ([RowListItem SourceAnn]
rowList, SourceType
rowTail) <- forall a. Type a -> ([RowListItem a], Type a)
rowToList SourceType
ty -> do
SourceType
kr <- forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind (forall a b. (a, b) -> a
fst SourceAnn
ann)
[RowListItem SourceAnn]
rowList' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [RowListItem SourceAnn]
rowList forall a b. (a -> b) -> a -> b
$ \(RowListItem SourceAnn
a Label
lbl SourceType
t) ->
forall a. a -> Label -> Type a -> RowListItem a
RowListItem SourceAnn
a Label
lbl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind SourceType
t SourceType
kr
SourceType
rowTail' <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind SourceType
rowTail forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType
E.kindRow SourceType
kr
SourceType
kr' <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
kr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
rowList', SourceType
rowTail'), SourceType -> SourceType
E.kindRow SourceType
kr' forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
TypeApp SourceAnn
ann SourceType
t1 SourceType
t2 -> do
(SourceType
t1', SourceType
k1) <- SourceType -> m (SourceType, SourceType)
go SourceType
t1
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceAnn
-> (SourceType, SourceType)
-> SourceType
-> m (SourceType, SourceType)
inferAppKind SourceAnn
ann (SourceType
t1', SourceType
k1) SourceType
t2
KindApp SourceAnn
ann SourceType
t1 SourceType
t2 -> do
(SourceType
t1', SourceType
kind) <- forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SourceType -> m (SourceType, SourceType)
go SourceType
t1
case SourceType
kind of
ForAll SourceAnn
_ TypeVarVisibility
_ Text
arg (Just SourceType
argKind) SourceType
resKind Maybe SkolemScope
_ -> do
SourceType
t2' <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind SourceType
t2 SourceType
argKind
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Type a -> Type a -> Type a
KindApp SourceAnn
ann SourceType
t1' SourceType
t2', forall a. Text -> Type a -> Type a -> Type a
replaceTypeVars Text
arg SourceType
t2' SourceType
resKind)
SourceType
_ ->
forall a. HasCallStack => String -> a
internalError String
"inferKind: unkinded forall binder"
KindedType SourceAnn
_ SourceType
t1 SourceType
t2 -> do
SourceType
t2' <- forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SourceType -> m (SourceType, SourceType)
go SourceType
t2
SourceType
t1' <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind SourceType
t1 SourceType
t2'
SourceType
t2'' <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
t2'
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
t1', SourceType
t2'')
ForAll SourceAnn
ann TypeVarVisibility
vis Text
arg Maybe SourceType
mbKind SourceType
ty Maybe SkolemScope
sc -> do
ModuleName
moduleName <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
m ModuleName
unsafeCheckCurrentModule
SourceType
kind <- case Maybe SourceType
mbKind of
Just SourceType
k -> forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
checkIsSaturatedType SourceType
k
Maybe SourceType
Nothing -> forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind (forall a b. (a, b) -> a
fst SourceAnn
ann)
(SourceType
ty', [(Int, SourceType)]
unks) <- forall (m :: * -> *) a.
MonadState CheckState m =>
ModuleName -> [(ProperName 'TypeName, SourceType)] -> m a -> m a
bindLocalTypeVariables ModuleName
moduleName [(forall (a :: ProperNameType). Text -> ProperName a
ProperName Text
arg, SourceType
kind)] forall a b. (a -> b) -> a -> b
$ do
SourceType
ty' <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
checkIsSaturatedType SourceType
ty
[(Int, SourceType)]
unks <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
[Int] -> m [(Int, SourceType)]
unknownsWithKinds forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IS.toList forall a b. (a -> b) -> a -> b
$ forall a. Type a -> IntSet
unknowns SourceType
ty'
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty', [(Int, SourceType)]
unks)
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(Int, SourceType)]
unks forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadState CheckState m =>
Maybe UnkLevel -> Int -> SourceType -> m ()
addUnsolved forall a. Maybe a
Nothing
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a.
a
-> TypeVarVisibility
-> Text
-> Maybe (Type a)
-> Type a
-> Maybe SkolemScope
-> Type a
ForAll SourceAnn
ann TypeVarVisibility
vis Text
arg (forall a. a -> Maybe a
Just SourceType
kind) SourceType
ty' Maybe SkolemScope
sc, SourceType
E.kindType forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
ParensInType SourceAnn
_ SourceType
ty ->
SourceType -> m (SourceType, SourceType)
go SourceType
ty
SourceType
ty ->
forall a. HasCallStack => String -> a
internalError forall a b. (a -> b) -> a -> b
$ String
"inferKind: Unimplemented case \n" forall a. Semigroup a => a -> a -> a
<> forall a. Int -> Type a -> String
prettyPrintType Int
100 SourceType
ty
inferAppKind
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceAnn
-> (SourceType, SourceType)
-> SourceType
-> m (SourceType, SourceType)
inferAppKind :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceAnn
-> (SourceType, SourceType)
-> SourceType
-> m (SourceType, SourceType)
inferAppKind SourceAnn
ann (SourceType
fn, SourceType
fnKind) SourceType
arg = case SourceType
fnKind of
TypeApp SourceAnn
_ (TypeApp SourceAnn
_ SourceType
arrKind SourceType
argKind) SourceType
resKind | forall a b. Type a -> Type b -> Bool
eqType SourceType
arrKind SourceType
E.tyFunction -> do
Bool
expandSynonyms <- forall {a}. Type a -> m Bool
requiresSynonymsToExpand SourceType
fn
SourceType
arg' <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
Bool -> SourceType -> SourceType -> m SourceType
checkKind' Bool
expandSynonyms SourceType
arg SourceType
argKind
(forall a. a -> Type a -> Type a -> Type a
TypeApp SourceAnn
ann SourceType
fn SourceType
arg',) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
resKind
TUnknown SourceAnn
_ Int
u -> do
(UnkLevel
lvl, SourceType
_) <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
u
Int
u1 <- forall (m :: * -> *). MonadState CheckState m => m Int
freshUnknown
Int
u2 <- forall (m :: * -> *). MonadState CheckState m => m Int
freshUnknown
forall (m :: * -> *).
MonadState CheckState m =>
Maybe UnkLevel -> Int -> SourceType -> m ()
addUnsolved (forall a. a -> Maybe a
Just UnkLevel
lvl) Int
u1 SourceType
E.kindType
forall (m :: * -> *).
MonadState CheckState m =>
Maybe UnkLevel -> Int -> SourceType -> m ()
addUnsolved (forall a. a -> Maybe a
Just UnkLevel
lvl) Int
u2 SourceType
E.kindType
forall (m :: * -> *).
MonadState CheckState m =>
Int -> SourceType -> m ()
solve Int
u forall a b. (a -> b) -> a -> b
$ (forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u1 SourceType -> SourceType -> SourceType
E.-:> forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u2) forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
SourceType
arg' <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind SourceType
arg forall a b. (a -> b) -> a -> b
$ forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u1
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Type a -> Type a -> Type a
TypeApp SourceAnn
ann SourceType
fn SourceType
arg', forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u2)
ForAll SourceAnn
_ TypeVarVisibility
_ Text
a (Just SourceType
k) SourceType
ty Maybe SkolemScope
_ -> do
Int
u <- forall (m :: * -> *). MonadState CheckState m => m Int
freshUnknown
forall (m :: * -> *).
MonadState CheckState m =>
Maybe UnkLevel -> Int -> SourceType -> m ()
addUnsolved forall a. Maybe a
Nothing Int
u SourceType
k
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceAnn
-> (SourceType, SourceType)
-> SourceType
-> m (SourceType, SourceType)
inferAppKind SourceAnn
ann (forall a. a -> Type a -> Type a -> Type a
KindApp SourceAnn
ann SourceType
fn (forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u), forall a. Text -> Type a -> Type a -> Type a
replaceTypeVars Text
a (forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u) SourceType
ty) SourceType
arg
SourceType
_ ->
forall (m :: * -> *) a.
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m a
cannotApplyTypeToType SourceType
fn SourceType
arg
where
requiresSynonymsToExpand :: Type a -> m Bool
requiresSynonymsToExpand = \case
TypeConstructor a
_ Qualified (ProperName 'TypeName)
v -> forall k a. Ord k => k -> Map k a -> Bool
M.notMember Qualified (ProperName 'TypeName)
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. Environment
-> Map
(Qualified (ProperName 'TypeName))
([(Text, Maybe SourceType)], SourceType)
E.typeSynonyms forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadState CheckState m => m Environment
getEnv
TypeApp a
_ Type a
l Type a
_ -> Type a -> m Bool
requiresSynonymsToExpand Type a
l
KindApp a
_ Type a
l Type a
_ -> Type a -> m Bool
requiresSynonymsToExpand Type a
l
Type a
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
cannotApplyTypeToType
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceType
-> SourceType
-> m a
cannotApplyTypeToType :: forall (m :: * -> *) a.
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m a
cannotApplyTypeToType SourceType
fn SourceType
arg = do
SourceType
argKind <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (SourceType, SourceType)
inferKind SourceType
arg
SourceType
_ <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind SourceType
fn forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceType -> SourceType -> SourceType
srcTypeApp (SourceType -> SourceType -> SourceType
srcTypeApp SourceType
E.tyFunction SourceType
argKind) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind SourceSpan
nullSourceSpan
forall (m :: * -> *) a.
(MonadError MultipleErrors m, HasCallStack) =>
Text -> m a
internalCompilerError forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ String
"Cannot apply type to type: " forall a. Semigroup a => a -> a -> a
<> forall a. Type a -> String
debugType (SourceType -> SourceType -> SourceType
srcTypeApp SourceType
fn SourceType
arg)
cannotApplyKindToType
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceType
-> SourceType
-> m a
cannotApplyKindToType :: forall (m :: * -> *) a.
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m a
cannotApplyKindToType SourceType
poly SourceType
arg = do
let ann :: SourceAnn
ann = forall a. Type a -> a
getAnnForType SourceType
arg
SourceType
argKind <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (SourceType, SourceType)
inferKind SourceType
arg
SourceType
_ <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind SourceType
poly forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [(a, (Text, Maybe (Type a)))] -> Type a -> Type a
mkForAll [(SourceAnn
ann, (Text
"k", forall a. a -> Maybe a
Just SourceType
argKind))] forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind SourceSpan
nullSourceSpan
forall (m :: * -> *) a.
(MonadError MultipleErrors m, HasCallStack) =>
Text -> m a
internalCompilerError forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ String
"Cannot apply kind to type: " forall a. Semigroup a => a -> a -> a
<> forall a. Type a -> String
debugType (SourceType -> SourceType -> SourceType
srcKindApp SourceType
poly SourceType
arg)
checkKind
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceType
-> SourceType
-> m SourceType
checkKind :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
Bool -> SourceType -> SourceType -> m SourceType
checkKind' Bool
False
checkIsSaturatedType
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceType
-> m SourceType
checkIsSaturatedType :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
checkIsSaturatedType SourceType
ty = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
Bool -> SourceType -> SourceType -> m SourceType
checkKind' Bool
True SourceType
ty SourceType
E.kindType
checkKind'
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> Bool
-> SourceType
-> SourceType
-> m SourceType
checkKind' :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
Bool -> SourceType -> SourceType -> m SourceType
checkKind' Bool
requireSynonymsToExpand SourceType
ty SourceType
kind2 = do
forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint (SourceType -> SourceType -> ErrorMessageHint
ErrorCheckingKind SourceType
ty SourceType
kind2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
MonadError MultipleErrors m =>
SourceSpan -> m a -> m a
rethrowWithPosition (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. Type a -> a
getAnnForType SourceType
ty) forall a b. (a -> b) -> a -> b
$ do
(SourceType
ty', SourceType
kind1) <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (SourceType, SourceType)
inferKind SourceType
ty
SourceType
kind1' <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
kind1
SourceType
kind2' <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
kind2
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
requireSynonymsToExpand forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms SourceType
ty'
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
(SourceType, SourceType) -> SourceType -> m SourceType
instantiateKind (SourceType
ty', SourceType
kind1') SourceType
kind2'
instantiateKind
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> (SourceType, SourceType)
-> SourceType
-> m SourceType
instantiateKind :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
(SourceType, SourceType) -> SourceType -> m SourceType
instantiateKind (SourceType
ty, SourceType
kind1) SourceType
kind2 = case SourceType
kind1 of
ForAll SourceAnn
_ TypeVarVisibility
_ Text
a (Just SourceType
k) SourceType
t Maybe SkolemScope
_ | forall {a}. Type a -> Bool
shouldInstantiate SourceType
kind2 -> do
let ann :: SourceAnn
ann = forall a. Type a -> a
getAnnForType SourceType
ty
SourceType
u <- forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> SourceType -> m SourceType
freshKindWithKind (forall a b. (a, b) -> a
fst SourceAnn
ann) SourceType
k
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
(SourceType, SourceType) -> SourceType -> m SourceType
instantiateKind (forall a. a -> Type a -> Type a -> Type a
KindApp SourceAnn
ann SourceType
ty SourceType
u, forall a. Text -> Type a -> Type a -> Type a
replaceTypeVars Text
a SourceType
u SourceType
t) SourceType
kind2
SourceType
_ -> do
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
subsumesKind SourceType
kind1 SourceType
kind2
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
ty
where
shouldInstantiate :: Type a -> Bool
shouldInstantiate = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
ForAll a
_ TypeVarVisibility
_ Text
_ Maybe (Type a)
_ Type a
_ Maybe SkolemScope
_ -> Bool
True
Type a
_ -> Bool
False
subsumesKind
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceType
-> SourceType
-> m ()
subsumesKind :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
subsumesKind = SourceType -> SourceType -> m ()
go
where
go :: SourceType -> SourceType -> m ()
go = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
(TypeApp SourceAnn
_ (TypeApp SourceAnn
_ SourceType
arr1 SourceType
a1) SourceType
a2, TypeApp SourceAnn
_ (TypeApp SourceAnn
_ SourceType
arr2 SourceType
b1) SourceType
b2)
| forall a b. Type a -> Type b -> Bool
eqType SourceType
arr1 SourceType
E.tyFunction
, forall a b. Type a -> Type b -> Bool
eqType SourceType
arr2 SourceType
E.tyFunction -> do
SourceType -> SourceType -> m ()
go SourceType
b1 SourceType
a1
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> m ()
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
a2 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
b2
(SourceType
a, ForAll SourceAnn
ann TypeVarVisibility
_ Text
var Maybe SourceType
mbKind SourceType
b Maybe SkolemScope
mbScope) -> do
SkolemScope
scope <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall (m :: * -> *). MonadState CheckState m => m SkolemScope
newSkolemScope forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe SkolemScope
mbScope
Int
skolc <- forall (m :: * -> *). MonadState CheckState m => m Int
newSkolemConstant
SourceType -> SourceType -> m ()
go SourceType
a forall a b. (a -> b) -> a -> b
$ forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize SourceAnn
ann Text
var Maybe SourceType
mbKind Int
skolc SkolemScope
scope SourceType
b
(ForAll SourceAnn
ann TypeVarVisibility
_ Text
var (Just SourceType
kind) SourceType
a Maybe SkolemScope
_, SourceType
b) -> do
SourceType
a' <- forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> SourceType -> m SourceType
freshKindWithKind (forall a b. (a, b) -> a
fst SourceAnn
ann) SourceType
kind
SourceType -> SourceType -> m ()
go (forall a. Text -> Type a -> Type a -> Type a
replaceTypeVars Text
var SourceType
a' SourceType
a) SourceType
b
(TUnknown SourceAnn
ann Int
u, b :: SourceType
b@(TypeApp SourceAnn
_ (TypeApp SourceAnn
_ SourceType
arr SourceType
_) SourceType
_))
| forall a b. Type a -> Type b -> Bool
eqType SourceType
arr SourceType
E.tyFunction
, Int -> IntSet -> Bool
IS.notMember Int
u (forall a. Type a -> IntSet
unknowns SourceType
b) ->
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> m ()
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceAnn -> Int -> m SourceType
solveUnknownAsFunction SourceAnn
ann Int
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
b
(a :: SourceType
a@(TypeApp SourceAnn
_ (TypeApp SourceAnn
_ SourceType
arr SourceType
_) SourceType
_), TUnknown SourceAnn
ann Int
u)
| forall a b. Type a -> Type b -> Bool
eqType SourceType
arr SourceType
E.tyFunction
, Int -> IntSet -> Bool
IS.notMember Int
u (forall a. Type a -> IntSet
unknowns SourceType
a) ->
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> m ()
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceAnn -> Int -> m SourceType
solveUnknownAsFunction SourceAnn
ann Int
u
(SourceType
a, SourceType
b) ->
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
unifyKinds SourceType
a SourceType
b
unifyKinds
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceType
-> SourceType
-> m ()
unifyKinds :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
unifyKinds = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
(SourceType -> SourceType -> m ())
-> SourceType -> SourceType -> m ()
unifyKindsWithFailure forall a b. (a -> b) -> a -> b
$ \SourceType
w1 SourceType
w2 ->
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SourceSpan] -> SimpleErrorMessage -> MultipleErrors
errorMessage''' (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a
getAnnForType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SourceType
w1, SourceType
w2])
forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> SimpleErrorMessage
KindsDoNotUnify SourceType
w1 SourceType
w2
unifyKinds'
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceType
-> SourceType
-> m ()
unifyKinds' :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
unifyKinds' = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
(SourceType -> SourceType -> m ())
-> SourceType -> SourceType -> m ()
unifyKindsWithFailure forall a b. (a -> b) -> a -> b
$ \SourceType
w1 SourceType
w2 ->
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage
forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> SimpleErrorMessage
KindsDoNotUnify SourceType
w1 SourceType
w2
checkTypeKind
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceType
-> SourceType
-> m ()
checkTypeKind :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
checkTypeKind SourceType
ty SourceType
kind =
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
(SourceType -> SourceType -> m ())
-> SourceType -> SourceType -> m ()
unifyKindsWithFailure (\SourceType
_ SourceType
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> SimpleErrorMessage
ExpectedType SourceType
ty SourceType
kind) SourceType
kind SourceType
E.kindType
unifyKindsWithFailure
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> (SourceType -> SourceType -> m ())
-> SourceType
-> SourceType
-> m ()
unifyKindsWithFailure :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
(SourceType -> SourceType -> m ())
-> SourceType -> SourceType -> m ()
unifyKindsWithFailure SourceType -> SourceType -> m ()
onFailure = SourceType -> SourceType -> m ()
go
where
goWithLabel :: Label -> SourceType -> SourceType -> m ()
goWithLabel Label
l SourceType
t1 SourceType
t2 = forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint (Label -> ErrorMessageHint
ErrorInRowLabel Label
l) forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> m ()
go SourceType
t1 SourceType
t2
go :: SourceType -> SourceType -> m ()
go = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
(TypeApp SourceAnn
_ SourceType
p1 SourceType
p2, TypeApp SourceAnn
_ SourceType
p3 SourceType
p4) -> do
SourceType -> SourceType -> m ()
go SourceType
p1 SourceType
p3
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> m ()
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
p2 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
p4
(KindApp SourceAnn
_ SourceType
p1 SourceType
p2, KindApp SourceAnn
_ SourceType
p3 SourceType
p4) -> do
SourceType -> SourceType -> m ()
go SourceType
p1 SourceType
p3
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> m ()
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
p2 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
p4
(r1 :: SourceType
r1@(RCons SourceAnn
_ Label
_ SourceType
_ SourceType
_), SourceType
r2) ->
SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2
(SourceType
r1, r2 :: SourceType
r2@(RCons SourceAnn
_ Label
_ SourceType
_ SourceType
_)) ->
SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2
(r1 :: SourceType
r1@(REmpty SourceAnn
_), SourceType
r2) ->
SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2
(SourceType
r1, r2 :: SourceType
r2@(REmpty SourceAnn
_)) ->
SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2
(SourceType
w1, SourceType
w2) | forall a b. Type a -> Type b -> Bool
eqType SourceType
w1 SourceType
w2 ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
(TUnknown SourceAnn
_ Int
a', SourceType
p1) ->
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
Int -> SourceType -> m ()
solveUnknown Int
a' SourceType
p1
(SourceType
p1, TUnknown SourceAnn
_ Int
a') ->
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
Int -> SourceType -> m ()
solveUnknown Int
a' SourceType
p1
(SourceType
w1, SourceType
w2) ->
SourceType -> SourceType -> m ()
onFailure SourceType
w1 SourceType
w2
unifyRows :: SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2 = do
let ([m ()]
matches, (([RowListItem SourceAnn], SourceType),
([RowListItem SourceAnn], SourceType))
rest) = forall a r.
(Label -> Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith Label -> SourceType -> SourceType -> m ()
goWithLabel SourceType
r1 SourceType
r2
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
matches
(([RowListItem SourceAnn], SourceType),
([RowListItem SourceAnn], SourceType))
-> m ()
unifyTails (([RowListItem SourceAnn], SourceType),
([RowListItem SourceAnn], SourceType))
rest
unifyTails :: (([RowListItem SourceAnn], SourceType),
([RowListItem SourceAnn], SourceType))
-> m ()
unifyTails = \case
(([], TUnknown SourceAnn
_ Int
a'), ([RowListItem SourceAnn]
rs, SourceType
p1)) ->
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
Int -> SourceType -> m ()
solveUnknown Int
a' forall a b. (a -> b) -> a -> b
$ forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
rs, SourceType
p1)
(([RowListItem SourceAnn]
rs, SourceType
p1), ([], TUnknown SourceAnn
_ Int
a')) ->
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
Int -> SourceType -> m ()
solveUnknown Int
a' forall a b. (a -> b) -> a -> b
$ forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
rs, SourceType
p1)
(([], SourceType
w1), ([], SourceType
w2)) | forall a b. Type a -> Type b -> Bool
eqType SourceType
w1 SourceType
w2 ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
(([RowListItem SourceAnn]
rs1, TUnknown SourceAnn
_ Int
u1), ([RowListItem SourceAnn]
rs2, TUnknown SourceAnn
_ Int
u2)) | Int
u1 forall a. Eq a => a -> a -> Bool
/= Int
u2 -> do
SourceType
rest <- forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind SourceSpan
nullSourceSpan
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
Int -> SourceType -> m ()
solveUnknown Int
u1 forall a b. (a -> b) -> a -> b
$ forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
rs2, SourceType
rest)
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
Int -> SourceType -> m ()
solveUnknown Int
u2 forall a b. (a -> b) -> a -> b
$ forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
rs1, SourceType
rest)
(([RowListItem SourceAnn], SourceType)
w1, ([RowListItem SourceAnn], SourceType)
w2) ->
SourceType -> SourceType -> m ()
onFailure (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn], SourceType)
w1) (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn], SourceType)
w2)
solveUnknown
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> Unknown
-> SourceType
-> m ()
solveUnknown :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
Int -> SourceType -> m ()
solveUnknown Int
a' SourceType
p1 = do
SourceType
p2 <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
Int -> SourceType -> m SourceType
promoteKind Int
a' SourceType
p1
SourceType
w1 <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
a'
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
unifyKinds forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
w1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
elaborateKind SourceType
p2
forall (m :: * -> *).
MonadState CheckState m =>
Int -> SourceType -> m ()
solve Int
a' SourceType
p2
solveUnknownAsFunction
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceAnn
-> Unknown
-> m SourceType
solveUnknownAsFunction :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceAnn -> Int -> m SourceType
solveUnknownAsFunction SourceAnn
ann Int
u = do
UnkLevel
lvl <- forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
u
Int
u1 <- forall (m :: * -> *). MonadState CheckState m => m Int
freshUnknown
Int
u2 <- forall (m :: * -> *). MonadState CheckState m => m Int
freshUnknown
forall (m :: * -> *).
MonadState CheckState m =>
Maybe UnkLevel -> Int -> SourceType -> m ()
addUnsolved (forall a. a -> Maybe a
Just UnkLevel
lvl) Int
u1 SourceType
E.kindType
forall (m :: * -> *).
MonadState CheckState m =>
Maybe UnkLevel -> Int -> SourceType -> m ()
addUnsolved (forall a. a -> Maybe a
Just UnkLevel
lvl) Int
u2 SourceType
E.kindType
let uarr :: SourceType
uarr = (forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u1 SourceType -> SourceType -> SourceType
E.-:> forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u2) forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
forall (m :: * -> *).
MonadState CheckState m =>
Int -> SourceType -> m ()
solve Int
u SourceType
uarr
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
uarr
promoteKind
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> Unknown
-> SourceType
-> m SourceType
promoteKind :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
Int -> SourceType -> m SourceType
promoteKind Int
u2 SourceType
ty = do
UnkLevel
lvl2 <- forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
u2
forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) a.
Monad m =>
(Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereOnTypesM SourceType
ty forall a b. (a -> b) -> a -> b
$ \case
ty' :: SourceType
ty'@(TUnknown SourceAnn
ann Int
u1) -> do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
u1 forall a. Eq a => a -> a -> Bool
== Int
u2) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceType -> SimpleErrorMessage
InfiniteKind forall a b. (a -> b) -> a -> b
$ SourceType
ty
(UnkLevel
lvl1, SourceType
k) <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
u1
if UnkLevel
lvl1 forall a. Ord a => a -> a -> Bool
< UnkLevel
lvl2 then
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
ty'
else do
SourceType
k' <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
Int -> SourceType -> m SourceType
promoteKind Int
u2 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
k
Int
u1' <- forall (m :: * -> *). MonadState CheckState m => m Int
freshUnknown
forall (m :: * -> *).
MonadState CheckState m =>
Maybe UnkLevel -> Int -> SourceType -> m ()
addUnsolved (forall a. a -> Maybe a
Just UnkLevel
lvl2) Int
u1' SourceType
k'
forall (m :: * -> *).
MonadState CheckState m =>
Int -> SourceType -> m ()
solve Int
u1 forall a b. (a -> b) -> a -> b
$ forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u1'
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u1'
SourceType
ty' ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
ty'
elaborateKind
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceType
-> m SourceType
elaborateKind :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
elaborateKind = \case
TypeLevelString SourceAnn
ann PSString
_ ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType
E.kindSymbol forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
TypeLevelInt SourceAnn
ann Integer
_ ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType
E.tyInt forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
TypeConstructor SourceAnn
ann Qualified (ProperName 'TypeName)
v -> do
Environment
env <- forall (m :: * -> *). MonadState CheckState m => m Environment
getEnv
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'TypeName)
v (Environment
-> Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
E.types Environment
env) of
Maybe (SourceType, TypeKind)
Nothing ->
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' (forall a b. (a, b) -> a
fst SourceAnn
ann) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Qualified Name -> SimpleErrorMessage
UnknownName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProperName 'TypeName -> Name
TyName forall a b. (a -> b) -> a -> b
$ Qualified (ProperName 'TypeName)
v
Just (SourceType
kind, TypeKind
_) ->
(forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
kind
TypeVar SourceAnn
ann Text
a -> do
ModuleName
moduleName <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
m ModuleName
unsafeCheckCurrentModule
SourceType
kind <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
ModuleName -> Qualified (ProperName 'TypeName) -> m SourceType
lookupTypeVariable ModuleName
moduleName (forall a. QualifiedBy -> a -> Qualified a
Qualified QualifiedBy
ByNullSourcePos forall a b. (a -> b) -> a -> b
$ forall (a :: ProperNameType). Text -> ProperName a
ProperName Text
a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
kind forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
(Skolem SourceAnn
ann Text
_ Maybe SourceType
mbK Int
_ SkolemScope
_) -> do
SourceType
kind <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
internalError String
"Skolem has no kind") Maybe SourceType
mbK
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType
kind forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
TUnknown SourceAnn
ann Int
a' -> do
SourceType
kind <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
a'
(forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
kind
REmpty SourceAnn
ann -> do
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType
E.kindOfREmpty forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
RCons SourceAnn
ann Label
_ SourceType
t1 SourceType
_ -> do
SourceType
k1 <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
elaborateKind SourceType
t1
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType
E.kindRow SourceType
k1 forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
ty :: SourceType
ty@(TypeApp SourceAnn
ann SourceType
t1 SourceType
t2) -> do
SourceType
k1 <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
elaborateKind SourceType
t1
case SourceType
k1 of
TypeApp SourceAnn
_ (TypeApp SourceAnn
_ SourceType
k SourceType
_) SourceType
w2 | forall a b. Type a -> Type b -> Bool
eqType SourceType
k SourceType
E.tyFunction -> do
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType
w2 forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
TUnknown SourceAnn
a Int
u -> do
SourceType
_ <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceAnn -> Int -> m SourceType
solveUnknownAsFunction SourceAnn
a Int
u
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
elaborateKind SourceType
ty
SourceType
_ ->
forall (m :: * -> *) a.
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m a
cannotApplyTypeToType SourceType
t1 SourceType
t2
KindApp SourceAnn
ann SourceType
t1 SourceType
t2 -> do
SourceType
k1 <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
elaborateKind SourceType
t1
case SourceType
k1 of
ForAll SourceAnn
_ TypeVarVisibility
_ Text
a Maybe SourceType
_ SourceType
n Maybe SkolemScope
_ -> do
forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall a. Text -> Type a -> Type a -> Type a
replaceTypeVars Text
a) SourceType
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
t2
SourceType
_ ->
forall (m :: * -> *) a.
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m a
cannotApplyKindToType SourceType
t1 SourceType
t2
ForAll SourceAnn
ann TypeVarVisibility
_ Text
_ Maybe SourceType
_ SourceType
_ Maybe SkolemScope
_ -> do
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType
E.kindType forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
ConstrainedType SourceAnn
ann Constraint SourceAnn
_ SourceType
_ ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType
E.kindType forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
KindedType SourceAnn
ann SourceType
_ SourceType
k ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType
k forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
SourceType
ty ->
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' (forall a b. (a, b) -> a
fst (forall a. Type a -> a
getAnnForType SourceType
ty)) forall a b. (a -> b) -> a -> b
$ SourceType -> SimpleErrorMessage
UnsupportedTypeInKind SourceType
ty
checkEscapedSkolems :: MonadError MultipleErrors m => SourceType -> m ()
checkEscapedSkolems :: forall (m :: * -> *).
MonadError MultipleErrors m =>
SourceType -> m ()
checkEscapedSkolems SourceType
ty =
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SourceSpan, Text, SourceType) -> MultipleErrors
toSkolemError)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s r a.
s -> r -> (r -> r -> r) -> (s -> Type a -> (s, r)) -> Type a -> r
everythingWithContextOnTypes SourceType
ty [] forall a. Semigroup a => a -> a -> a
(<>) SourceType
-> SourceType -> (SourceType, [(SourceSpan, Text, SourceType)])
go
forall a b. (a -> b) -> a -> b
$ SourceType
ty
where
go :: SourceType -> SourceType -> (SourceType, [(SourceSpan, Text, SourceType)])
go :: SourceType
-> SourceType -> (SourceType, [(SourceSpan, Text, SourceType)])
go SourceType
ty' = \case
Skolem SourceAnn
ss Text
name Maybe SourceType
_ Int
_ SkolemScope
_ -> (SourceType
ty', [(forall a b. (a, b) -> a
fst SourceAnn
ss, Text
name, SourceType
ty')])
ty'' :: SourceType
ty''@(KindApp SourceAnn
_ SourceType
_ SourceType
_) -> (SourceType
ty'', [])
SourceType
_ -> (SourceType
ty', [])
toSkolemError :: (SourceSpan, Text, SourceType) -> MultipleErrors
toSkolemError (SourceSpan
ss, Text
name, SourceType
ty') =
SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. Type a -> a
getAnnForType SourceType
ty') forall a b. (a -> b) -> a -> b
$ Text -> Maybe SourceSpan -> SourceType -> SimpleErrorMessage
EscapedSkolem Text
name (forall a. a -> Maybe a
Just SourceSpan
ss) SourceType
ty'
kindOfWithUnknowns
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceType
-> m (([(Unknown, SourceType)], SourceType), SourceType)
kindOfWithUnknowns :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (([(Int, SourceType)], SourceType), SourceType)
kindOfWithUnknowns SourceType
ty = do
(SourceType
ty', SourceType
kind) <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (SourceType, SourceType)
kindOf SourceType
ty
[(Int, SourceType)]
unks <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
[Int] -> m [(Int, SourceType)]
unknownsWithKinds forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IS.toList forall a b. (a -> b) -> a -> b
$ forall a. Type a -> IntSet
unknowns SourceType
ty'
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([(Int, SourceType)]
unks, SourceType
ty'), SourceType
kind)
kindOf
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceType
-> m (SourceType, SourceType)
kindOf :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (SourceType, SourceType)
kindOf = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (([(Text, SourceType)], SourceType), SourceType)
kindOfWithScopedVars
kindOfWithScopedVars
:: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
=> SourceType
-> m (([(Text, SourceType)], SourceType), SourceType)
kindOfWithScopedVars :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (([(Text, SourceType)], SourceType), SourceType)
kindOfWithScopedVars SourceType
ty = do
(SourceType
ty', SourceType
kind) <- forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply (forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (SourceType, SourceType)
inferKind SourceType
ty
let binders :: [(SourceAnn, (Text, SourceType))]
binders = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall a. Type a -> Maybe ([(a, (Text, Type a))], Type a)
completeBinderList SourceType
ty'
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SourceAnn, (Text, SourceType))]
binders, SourceType
ty'), SourceType
kind)
type DataDeclarationArgs =
( SourceAnn
, ProperName 'TypeName
, [(Text, Maybe SourceType)]
, [DataConstructorDeclaration]
)
type DataDeclarationResult =
( [(DataConstructorDeclaration, SourceType)]
, SourceType
)
kindOfData
:: forall m. (MonadError MultipleErrors m, MonadState CheckState m)
=> ModuleName
-> DataDeclarationArgs
-> m DataDeclarationResult
kindOfData :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModuleName -> DataDeclarationArgs -> m DataDeclarationResult
kindOfData ModuleName
moduleName DataDeclarationArgs
dataDecl =
forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall s t a b. Field2 s t a b => Lens s t a b
_2) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModuleName
-> [TypeDeclarationArgs]
-> [DataDeclarationArgs]
-> [ClassDeclarationArgs]
-> m ([(SourceType, SourceType)], [DataDeclarationResult],
[ClassDeclarationResult])
kindsOfAll ModuleName
moduleName [] [DataDeclarationArgs
dataDecl] []
inferDataDeclaration
:: forall m. (MonadError MultipleErrors m, MonadState CheckState m)
=> ModuleName
-> DataDeclarationArgs
-> m [(DataConstructorDeclaration, SourceType)]
inferDataDeclaration :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModuleName
-> DataDeclarationArgs
-> m [(DataConstructorDeclaration, SourceType)]
inferDataDeclaration ModuleName
moduleName (SourceAnn
ann, ProperName 'TypeName
tyName, [(Text, Maybe SourceType)]
tyArgs, [DataConstructorDeclaration]
ctors) = do
SourceType
tyKind <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
ModuleName -> Qualified (ProperName 'TypeName) -> m SourceType
lookupTypeVariable ModuleName
moduleName (forall a. QualifiedBy -> a -> Qualified a
Qualified QualifiedBy
ByNullSourcePos ProperName 'TypeName
tyName)
let ([(SourceAnn, (Text, SourceType))]
sigBinders, SourceType
tyKind') = forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> Maybe ([(a, (Text, Type a))], Type a)
completeBinderList forall a b. (a -> b) -> a -> b
$ SourceType
tyKind
forall (m :: * -> *) a.
MonadState CheckState m =>
ModuleName -> [(ProperName 'TypeName, SourceType)] -> m a -> m a
bindLocalTypeVariables ModuleName
moduleName (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall (a :: ProperNameType). Text -> ProperName a
ProperName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SourceAnn, (Text, SourceType))]
sigBinders) forall a b. (a -> b) -> a -> b
$ do
[(Text, SourceType)]
tyArgs' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(Text, Maybe SourceType)]
tyArgs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind (forall a b. (a, b) -> a
fst SourceAnn
ann)) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
checkIsSaturatedType
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
subsumesKind (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SourceType -> SourceType -> SourceType
(E.-:>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) SourceType
E.kindType [(Text, SourceType)]
tyArgs') SourceType
tyKind'
forall (m :: * -> *) a.
MonadState CheckState m =>
ModuleName -> [(ProperName 'TypeName, SourceType)] -> m a -> m a
bindLocalTypeVariables ModuleName
moduleName (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall (a :: ProperNameType). Text -> ProperName a
ProperName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, SourceType)]
tyArgs') forall a b. (a -> b) -> a -> b
$ do
let tyCtorName :: SourceType
tyCtorName = Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor forall a b. (a -> b) -> a -> b
$ forall a. a -> ModuleName -> Qualified a
mkQualified ProperName 'TypeName
tyName ModuleName
moduleName
tyCtor :: SourceType
tyCtor = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\SourceType
ty -> SourceType -> SourceType -> SourceType
srcKindApp SourceType
ty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> SourceType
srcTypeVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) SourceType
tyCtorName [(SourceAnn, (Text, SourceType))]
sigBinders
tyCtor' :: SourceType
tyCtor' = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\SourceType
ty -> SourceType -> SourceType -> SourceType
srcTypeApp SourceType
ty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> SourceType
srcTypeVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) SourceType
tyCtor [(Text, SourceType)]
tyArgs'
ctorBinders :: [(SourceAnn, (Text, Maybe SourceType))]
ctorBinders = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just)) forall a b. (a -> b) -> a -> b
$ [(SourceAnn, (Text, SourceType))]
sigBinders forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SourceAnn
nullSourceAnn,) [(Text, SourceType)]
tyArgs'
visibility :: [(Text, TypeVarVisibility)]
visibility = forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall a b. a -> b -> a
const TypeVarVisibility
TypeVarVisible) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Maybe SourceType)]
tyArgs
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [DataConstructorDeclaration]
ctors forall a b. (a -> b) -> a -> b
$
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. [(Text, TypeVarVisibility)] -> Type a -> Type a
addVisibility [(Text, TypeVarVisibility)]
visibility forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [(a, (Text, Maybe (Type a)))] -> Type a -> Type a
mkForAll [(SourceAnn, (Text, Maybe SourceType))]
ctorBinders)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType
-> DataConstructorDeclaration
-> m (DataConstructorDeclaration, SourceType)
inferDataConstructor SourceType
tyCtor'
inferDataConstructor
:: forall m. (MonadError MultipleErrors m, MonadState CheckState m)
=> SourceType
-> DataConstructorDeclaration
-> m (DataConstructorDeclaration, SourceType)
inferDataConstructor :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType
-> DataConstructorDeclaration
-> m (DataConstructorDeclaration, SourceType)
inferDataConstructor SourceType
tyCtor DataConstructorDeclaration{[(Ident, SourceType)]
SourceAnn
ProperName 'ConstructorName
dataCtorFields :: DataConstructorDeclaration -> [(Ident, SourceType)]
dataCtorName :: DataConstructorDeclaration -> ProperName 'ConstructorName
dataCtorAnn :: DataConstructorDeclaration -> SourceAnn
dataCtorFields :: [(Ident, SourceType)]
dataCtorName :: ProperName 'ConstructorName
dataCtorAnn :: SourceAnn
..} = do
[(Ident, SourceType)]
dataCtorFields' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
checkIsSaturatedType) [(Ident, SourceType)]
dataCtorFields
SourceType
dataCtor <- 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 (SourceType -> SourceType -> SourceType
(E.-:>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)) [(Ident, SourceType)]
dataCtorFields' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind SourceType
tyCtor SourceType
E.kindType
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( DataConstructorDeclaration { dataCtorFields :: [(Ident, SourceType)]
dataCtorFields = [(Ident, SourceType)]
dataCtorFields', SourceAnn
ProperName 'ConstructorName
dataCtorName :: ProperName 'ConstructorName
dataCtorAnn :: SourceAnn
dataCtorName :: ProperName 'ConstructorName
dataCtorAnn :: SourceAnn
.. }, SourceType
dataCtor )
type TypeDeclarationArgs =
( SourceAnn
, ProperName 'TypeName
, [(Text, Maybe SourceType)]
, SourceType
)
type TypeDeclarationResult =
( SourceType
, SourceType
)
kindOfTypeSynonym
:: forall m. (MonadError MultipleErrors m, MonadState CheckState m)
=> ModuleName
-> TypeDeclarationArgs
-> m TypeDeclarationResult
kindOfTypeSynonym :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModuleName -> TypeDeclarationArgs -> m (SourceType, SourceType)
kindOfTypeSynonym ModuleName
moduleName TypeDeclarationArgs
typeDecl =
forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall s t a b. Field1 s t a b => Lens s t a b
_1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModuleName
-> [TypeDeclarationArgs]
-> [DataDeclarationArgs]
-> [ClassDeclarationArgs]
-> m ([(SourceType, SourceType)], [DataDeclarationResult],
[ClassDeclarationResult])
kindsOfAll ModuleName
moduleName [TypeDeclarationArgs
typeDecl] [] []
inferTypeSynonym
:: forall m. (MonadError MultipleErrors m, MonadState CheckState m)
=> ModuleName
-> TypeDeclarationArgs
-> m SourceType
inferTypeSynonym :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModuleName -> TypeDeclarationArgs -> m SourceType
inferTypeSynonym ModuleName
moduleName (SourceAnn
ann, ProperName 'TypeName
tyName, [(Text, Maybe SourceType)]
tyArgs, SourceType
tyBody) = do
SourceType
tyKind <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
ModuleName -> Qualified (ProperName 'TypeName) -> m SourceType
lookupTypeVariable ModuleName
moduleName (forall a. QualifiedBy -> a -> Qualified a
Qualified QualifiedBy
ByNullSourcePos ProperName 'TypeName
tyName)
let ([(SourceAnn, (Text, SourceType))]
sigBinders, SourceType
tyKind') = forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> Maybe ([(a, (Text, Type a))], Type a)
completeBinderList forall a b. (a -> b) -> a -> b
$ SourceType
tyKind
forall (m :: * -> *) a.
MonadState CheckState m =>
ModuleName -> [(ProperName 'TypeName, SourceType)] -> m a -> m a
bindLocalTypeVariables ModuleName
moduleName (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall (a :: ProperNameType). Text -> ProperName a
ProperName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SourceAnn, (Text, SourceType))]
sigBinders) forall a b. (a -> b) -> a -> b
$ do
SourceType
kindRes <- forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind (forall a b. (a, b) -> a
fst SourceAnn
ann)
[(Text, SourceType)]
tyArgs' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(Text, Maybe SourceType)]
tyArgs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind (forall a b. (a, b) -> a
fst SourceAnn
ann)) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
checkIsSaturatedType
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
unifyKinds SourceType
tyKind' forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SourceType -> SourceType -> SourceType
(E.-:>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) SourceType
kindRes [(Text, SourceType)]
tyArgs'
forall (m :: * -> *) a.
MonadState CheckState m =>
ModuleName -> [(ProperName 'TypeName, SourceType)] -> m a -> m a
bindLocalTypeVariables ModuleName
moduleName (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall (a :: ProperNameType). Text -> ProperName a
ProperName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, SourceType)]
tyArgs') forall a b. (a -> b) -> a -> b
$ do
(SourceType, SourceType)
tyBodyAndKind <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (SourceType, SourceType)
inferKind SourceType
tyBody
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
(SourceType, SourceType) -> SourceType -> m SourceType
instantiateKind (SourceType, SourceType)
tyBodyAndKind forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
kindRes
checkQuantification
:: forall m. (MonadError MultipleErrors m)
=> SourceType
-> m ()
checkQuantification :: forall (m :: * -> *).
MonadError MultipleErrors m =>
SourceType -> m ()
checkQuantification =
forall {f :: * -> *} {t :: * -> *} {b}.
(Foldable t, MonadError MultipleErrors f) =>
t ((SourceSpan, b), Text) -> f ()
collectErrors forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a} {a}.
[(a, Text)] -> [Text] -> [(a, (Text, Type a))] -> [(a, Text)]
go [] [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> Maybe ([(a, (Text, Type a))], Type a)
completeBinderList
where
collectErrors :: t ((SourceSpan, b), Text) -> f ()
collectErrors t ((SourceSpan, b), Text)
vars =
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null t ((SourceSpan, b), Text)
vars)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\((SourceSpan, b)
ann, Text
arg) -> SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' (forall a b. (a, b) -> a
fst (SourceSpan, b)
ann) forall a b. (a -> b) -> a -> b
$ Text -> SimpleErrorMessage
QuantificationCheckFailureInKind Text
arg)
forall a b. (a -> b) -> a -> b
$ t ((SourceSpan, b), Text)
vars
go :: [(a, Text)] -> [Text] -> [(a, (Text, Type a))] -> [(a, Text)]
go [(a, Text)]
acc [Text]
_ [] = forall a. [a] -> [a]
reverse [(a, Text)]
acc
go [(a, Text)]
acc [Text]
sco ((a
_, (Text
arg, Type a
k)) : [(a, (Text, Type a))]
rest)
| Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [Text]
sco) forall a b. (a -> b) -> a -> b
$ forall a. Type a -> [Text]
freeTypeVariables Type a
k = forall {a} {a}.
[(a, Text)] -> Text -> [(a, (Text, Type a))] -> [(a, Text)]
goDeps [(a, Text)]
acc Text
arg [(a, (Text, Type a))]
rest
| Bool
otherwise = [(a, Text)] -> [Text] -> [(a, (Text, Type a))] -> [(a, Text)]
go [(a, Text)]
acc (Text
arg forall a. a -> [a] -> [a]
: [Text]
sco) [(a, (Text, Type a))]
rest
goDeps :: [(a, Text)] -> Text -> [(a, (Text, Type a))] -> [(a, Text)]
goDeps [(a, Text)]
acc Text
_ [] = [(a, Text)]
acc
goDeps [(a, Text)]
acc Text
karg ((a
ann, (Text
arg, Type a
k)) : [(a, (Text, Type a))]
rest)
| Bool
isDep Bool -> Bool -> Bool
&& Text
arg forall a. Eq a => a -> a -> Bool
== Text
karg = (a
ann, Text
arg) forall a. a -> [a] -> [a]
: [(a, Text)]
acc
| Bool
isDep = [(a, Text)] -> Text -> [(a, (Text, Type a))] -> [(a, Text)]
goDeps ((a
ann, Text
arg) forall a. a -> [a] -> [a]
: [(a, Text)]
acc) Text
karg [(a, (Text, Type a))]
rest
| Bool
otherwise = [(a, Text)] -> Text -> [(a, (Text, Type a))] -> [(a, Text)]
goDeps [(a, Text)]
acc Text
karg [(a, (Text, Type a))]
rest
where
isDep :: Bool
isDep =
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Text
karg forall a b. (a -> b) -> a -> b
$ forall a. Type a -> [Text]
freeTypeVariables Type a
k
checkVisibleTypeQuantification
:: forall m. (MonadError MultipleErrors m)
=> SourceType
-> m ()
checkVisibleTypeQuantification :: forall (m :: * -> *).
MonadError MultipleErrors m =>
SourceType -> m ()
checkVisibleTypeQuantification =
forall {f :: * -> *} {t :: * -> *}.
(Foldable t, MonadError MultipleErrors f) =>
t Text -> f ()
collectErrors forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> [Text]
freeTypeVariables
where
collectErrors :: t Text -> f ()
collectErrors t Text
vars =
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null t Text
vars)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (SimpleErrorMessage -> MultipleErrors
errorMessage forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> SimpleErrorMessage
VisibleQuantificationCheckFailureInType)
forall a b. (a -> b) -> a -> b
$ t Text
vars
checkTypeQuantification
:: forall m. (MonadError MultipleErrors m)
=> SourceType
-> m ()
checkTypeQuantification :: forall (m :: * -> *).
MonadError MultipleErrors m =>
SourceType -> m ()
checkTypeQuantification =
forall {f :: * -> *} {t :: * -> *}.
(Foldable t, MonadError MultipleErrors f) =>
t (SourceSpan, IntSet, SourceType) -> f ()
collectErrors forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s r a.
s -> r -> (r -> r -> r) -> (s -> Type a -> (s, r)) -> Type a -> r
everythingWithContextOnTypes Bool
True [] forall a. Semigroup a => a -> a -> a
(<>) forall {a} {b}.
Bool -> Type (a, b) -> (Bool, [(a, IntSet, Type (a, b))])
unknownsInKinds
where
collectErrors :: t (SourceSpan, IntSet, SourceType) -> f ()
collectErrors t (SourceSpan, IntSet, SourceType)
tysWithUnks =
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null t (SourceSpan, IntSet, SourceType)
tysWithUnks) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (SourceSpan, IntSet, SourceType) -> MultipleErrors
toMultipleErrors forall a b. (a -> b) -> a -> b
$ t (SourceSpan, IntSet, SourceType)
tysWithUnks
toMultipleErrors :: (SourceSpan, IntSet, SourceType) -> MultipleErrors
toMultipleErrors (SourceSpan
ss, IntSet
unks, SourceType
ty) =
SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' SourceSpan
ss forall a b. (a -> b) -> a -> b
$ [Int] -> SourceType -> SimpleErrorMessage
QuantificationCheckFailureInType (IntSet -> [Int]
IS.toList IntSet
unks) SourceType
ty
unknownsInKinds :: Bool -> Type (a, b) -> (Bool, [(a, IntSet, Type (a, b))])
unknownsInKinds Bool
False Type (a, b)
_ = (Bool
False, [])
unknownsInKinds Bool
_ Type (a, b)
ty = case Type (a, b)
ty of
ForAll (a, b)
sa TypeVarVisibility
_ Text
_ Maybe (Type (a, b))
_ Type (a, b)
_ Maybe SkolemScope
_ | IntSet
unks <- forall a. Type a -> IntSet
unknowns Type (a, b)
ty, Bool -> Bool
not (IntSet -> Bool
IS.null IntSet
unks) ->
(Bool
False, [(forall a b. (a, b) -> a
fst (a, b)
sa, IntSet
unks, Type (a, b)
ty)])
KindApp (a, b)
sa Type (a, b)
_ Type (a, b)
_ | IntSet
unks <- forall a. Type a -> IntSet
unknowns Type (a, b)
ty, Bool -> Bool
not (IntSet -> Bool
IS.null IntSet
unks) ->
(Bool
False, [(forall a b. (a, b) -> a
fst (a, b)
sa, IntSet
unks, Type (a, b)
ty)])
ConstrainedType (a, b)
sa Constraint (a, b)
_ Type (a, b)
_ | IntSet
unks <- forall a. Type a -> IntSet
unknowns Type (a, b)
ty, Bool -> Bool
not (IntSet -> Bool
IS.null IntSet
unks) ->
(Bool
False, [(forall a b. (a, b) -> a
fst (a, b)
sa, IntSet
unks, Type (a, b)
ty)])
Type (a, b)
_ ->
(Bool
True, [])
type ClassDeclarationArgs =
( SourceAnn
, ProperName 'ClassName
, [(Text, Maybe SourceType)]
, [SourceConstraint]
, [Declaration]
)
type ClassDeclarationResult =
( [(Text, SourceType)]
, [SourceConstraint]
, [Declaration]
, SourceType
)
kindOfClass
:: forall m. (MonadError MultipleErrors m, MonadState CheckState m)
=> ModuleName
-> ClassDeclarationArgs
-> m ClassDeclarationResult
kindOfClass :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModuleName -> ClassDeclarationArgs -> m ClassDeclarationResult
kindOfClass ModuleName
moduleName ClassDeclarationArgs
clsDecl =
forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall s t a b. Field3 s t a b => Lens s t a b
_3) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModuleName
-> [TypeDeclarationArgs]
-> [DataDeclarationArgs]
-> [ClassDeclarationArgs]
-> m ([(SourceType, SourceType)], [DataDeclarationResult],
[ClassDeclarationResult])
kindsOfAll ModuleName
moduleName [] [] [ClassDeclarationArgs
clsDecl]
inferClassDeclaration
:: forall m. (MonadError MultipleErrors m, MonadState CheckState m)
=> ModuleName
-> ClassDeclarationArgs
-> m ([(Text, SourceType)], [SourceConstraint], [Declaration])
inferClassDeclaration :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModuleName
-> ClassDeclarationArgs
-> m ([(Text, SourceType)], [Constraint SourceAnn], [Declaration])
inferClassDeclaration ModuleName
moduleName (SourceAnn
ann, ProperName 'ClassName
clsName, [(Text, Maybe SourceType)]
clsArgs, [Constraint SourceAnn]
superClasses, [Declaration]
decls) = do
SourceType
clsKind <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
ModuleName -> Qualified (ProperName 'TypeName) -> m SourceType
lookupTypeVariable ModuleName
moduleName (forall a. QualifiedBy -> a -> Qualified a
Qualified QualifiedBy
ByNullSourcePos forall a b. (a -> b) -> a -> b
$ forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a -> ProperName b
coerceProperName ProperName 'ClassName
clsName)
let ([(SourceAnn, (Text, SourceType))]
sigBinders, SourceType
clsKind') = forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> Maybe ([(a, (Text, Type a))], Type a)
completeBinderList forall a b. (a -> b) -> a -> b
$ SourceType
clsKind
forall (m :: * -> *) a.
MonadState CheckState m =>
ModuleName -> [(ProperName 'TypeName, SourceType)] -> m a -> m a
bindLocalTypeVariables ModuleName
moduleName (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall (a :: ProperNameType). Text -> ProperName a
ProperName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SourceAnn, (Text, SourceType))]
sigBinders) forall a b. (a -> b) -> a -> b
$ do
[(Text, SourceType)]
clsArgs' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(Text, Maybe SourceType)]
clsArgs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind (forall a b. (a, b) -> a
fst SourceAnn
ann)) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
checkIsSaturatedType
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
unifyKinds SourceType
clsKind' forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SourceType -> SourceType -> SourceType
(E.-:>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) SourceType
E.kindConstraint [(Text, SourceType)]
clsArgs'
forall (m :: * -> *) a.
MonadState CheckState m =>
ModuleName -> [(ProperName 'TypeName, SourceType)] -> m a -> m a
bindLocalTypeVariables ModuleName
moduleName (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall (a :: ProperNameType). Text -> ProperName a
ProperName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, SourceType)]
clsArgs') forall a b. (a -> b) -> a -> b
$ do
([(Text, SourceType)]
clsArgs',,)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Constraint SourceAnn]
superClasses forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Constraint SourceAnn -> m (Constraint SourceAnn)
checkConstraint
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Declaration]
decls forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Declaration -> m Declaration
checkClassMemberDeclaration
checkClassMemberDeclaration
:: forall m. (MonadError MultipleErrors m, MonadState CheckState m)
=> Declaration
-> m Declaration
checkClassMemberDeclaration :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Declaration -> m Declaration
checkClassMemberDeclaration = \case
TypeDeclaration (TypeDeclarationData SourceAnn
ann Ident
ident SourceType
ty) ->
TypeDeclarationData -> Declaration
TypeDeclaration forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceAnn -> Ident -> SourceType -> TypeDeclarationData
TypeDeclarationData SourceAnn
ann Ident
ident forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind SourceType
ty SourceType
E.kindType
Declaration
_ -> forall a. HasCallStack => String -> a
internalError String
"Invalid class member declaration"
applyClassMemberDeclaration
:: forall m. (MonadError MultipleErrors m, MonadState CheckState m)
=> Declaration
-> m Declaration
applyClassMemberDeclaration :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Declaration -> m Declaration
applyClassMemberDeclaration = \case
TypeDeclaration (TypeDeclarationData SourceAnn
ann Ident
ident SourceType
ty) ->
TypeDeclarationData -> Declaration
TypeDeclaration forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceAnn -> Ident -> SourceType -> TypeDeclarationData
TypeDeclarationData SourceAnn
ann Ident
ident forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
ty
Declaration
_ -> forall a. HasCallStack => String -> a
internalError String
"Invalid class member declaration"
mapTypeDeclaration :: (SourceType -> SourceType) -> Declaration -> Declaration
mapTypeDeclaration :: (SourceType -> SourceType) -> Declaration -> Declaration
mapTypeDeclaration SourceType -> SourceType
f = \case
TypeDeclaration (TypeDeclarationData SourceAnn
ann Ident
ident SourceType
ty) ->
TypeDeclarationData -> Declaration
TypeDeclaration forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceAnn -> Ident -> SourceType -> TypeDeclarationData
TypeDeclarationData SourceAnn
ann Ident
ident forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType
f SourceType
ty
Declaration
other ->
Declaration
other
checkConstraint
:: forall m. (MonadError MultipleErrors m, MonadState CheckState m)
=> SourceConstraint
-> m SourceConstraint
checkConstraint :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Constraint SourceAnn -> m (Constraint SourceAnn)
checkConstraint (Constraint SourceAnn
ann Qualified (ProperName 'ClassName)
clsName [SourceType]
kinds [SourceType]
args Maybe ConstraintData
dat) = do
let ty :: SourceType
ty = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a. a -> Type a -> Type a -> Type a
TypeApp SourceAnn
ann) (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a. a -> Type a -> Type a -> Type a
KindApp SourceAnn
ann) (forall a. a -> Qualified (ProperName 'TypeName) -> Type a
TypeConstructor SourceAnn
ann (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a -> ProperName b
coerceProperName Qualified (ProperName 'ClassName)
clsName)) [SourceType]
kinds) [SourceType]
args
(SourceType
_, [SourceType]
kinds', [SourceType]
args') <- forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind SourceType
ty SourceType
E.kindConstraint
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a.
a
-> Qualified (ProperName 'ClassName)
-> [Type a]
-> [Type a]
-> Maybe ConstraintData
-> Constraint a
Constraint SourceAnn
ann Qualified (ProperName 'ClassName)
clsName [SourceType]
kinds' [SourceType]
args' Maybe ConstraintData
dat
applyConstraint
:: forall m. (MonadError MultipleErrors m, MonadState CheckState m)
=> SourceConstraint
-> m SourceConstraint
applyConstraint :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Constraint SourceAnn -> m (Constraint SourceAnn)
applyConstraint (Constraint SourceAnn
ann Qualified (ProperName 'ClassName)
clsName [SourceType]
kinds [SourceType]
args Maybe ConstraintData
dat) = do
let ty :: SourceType
ty = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a. a -> Type a -> Type a -> Type a
TypeApp SourceAnn
ann) (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a. a -> Type a -> Type a -> Type a
KindApp SourceAnn
ann) (forall a. a -> Qualified (ProperName 'TypeName) -> Type a
TypeConstructor SourceAnn
ann (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a -> ProperName b
coerceProperName Qualified (ProperName 'ClassName)
clsName)) [SourceType]
kinds) [SourceType]
args
(SourceType
_, [SourceType]
kinds', [SourceType]
args') <- forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
ty
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a.
a
-> Qualified (ProperName 'ClassName)
-> [Type a]
-> [Type a]
-> Maybe ConstraintData
-> Constraint a
Constraint SourceAnn
ann Qualified (ProperName 'ClassName)
clsName [SourceType]
kinds' [SourceType]
args' Maybe ConstraintData
dat
type InstanceDeclarationArgs =
( SourceAnn
, [SourceConstraint]
, Qualified (ProperName 'ClassName)
, [SourceType]
)
type InstanceDeclarationResult =
( [SourceConstraint]
, [SourceType]
, [SourceType]
, [(Text, SourceType)]
)
checkInstanceDeclaration
:: forall m. (MonadError MultipleErrors m, MonadState CheckState m)
=> ModuleName
-> InstanceDeclarationArgs
-> m InstanceDeclarationResult
checkInstanceDeclaration :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModuleName
-> InstanceDeclarationArgs -> m InstanceDeclarationResult
checkInstanceDeclaration ModuleName
moduleName (SourceAnn
ann, [Constraint SourceAnn]
constraints, Qualified (ProperName 'ClassName)
clsName, [SourceType]
args) = do
let ty :: SourceType
ty = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a. a -> Type a -> Type a -> Type a
TypeApp SourceAnn
ann) (forall a. a -> Qualified (ProperName 'TypeName) -> Type a
TypeConstructor SourceAnn
ann (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a -> ProperName b
coerceProperName Qualified (ProperName 'ClassName)
clsName)) [SourceType]
args
tyWithConstraints :: SourceType
tyWithConstraints = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Constraint SourceAnn -> SourceType -> SourceType
srcConstrainedType SourceType
ty [Constraint SourceAnn]
constraints
freeVars :: [Text]
freeVars = forall a. Type a -> [Text]
freeTypeVariables SourceType
tyWithConstraints
[(ProperName 'TypeName, SourceType)]
freeVarsDict <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Text]
freeVars forall a b. (a -> b) -> a -> b
$ \Text
v -> (forall (a :: ProperNameType). Text -> ProperName a
ProperName Text
v,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind (forall a b. (a, b) -> a
fst SourceAnn
ann)
forall (m :: * -> *) a.
MonadState CheckState m =>
ModuleName -> [(ProperName 'TypeName, SourceType)] -> m a -> m a
bindLocalTypeVariables ModuleName
moduleName [(ProperName 'TypeName, SourceType)]
freeVarsDict forall a b. (a -> b) -> a -> b
$ do
SourceType
ty' <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind SourceType
ty SourceType
E.kindConstraint
[Constraint SourceAnn]
constraints' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Constraint SourceAnn]
constraints forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Constraint SourceAnn -> m (Constraint SourceAnn)
checkConstraint
SourceType
allTy <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Constraint SourceAnn -> SourceType -> SourceType
srcConstrainedType SourceType
ty' [Constraint SourceAnn]
constraints'
[(Int, SourceType)]
allUnknowns <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
[Int] -> m [(Int, SourceType)]
unknownsWithKinds forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IS.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. Type a -> IntSet
unknowns forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SourceType
allTy forall a. a -> [a] -> [a]
:) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(ProperName 'TypeName, SourceType)]
freeVarsDict
let unknownVars :: [(Int, (Text, SourceType))]
unknownVars = [Text] -> [(Int, SourceType)] -> [(Int, (Text, SourceType))]
unknownVarNames (forall a. Type a -> [Text]
usedTypeVariables SourceType
allTy) [(Int, SourceType)]
allUnknowns
let allWithVars :: SourceType
allWithVars = forall a. [(Int, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars [(Int, (Text, SourceType))]
unknownVars SourceType
allTy
let ([Constraint SourceAnn]
allConstraints, (SourceType
_, [SourceType]
allKinds, [SourceType]
allArgs)) = forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Type a -> ([Constraint a], Type a)
unapplyConstraints SourceType
allWithVars
[(Text, SourceType)]
varKinds <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. [(Int, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars [(Int, (Text, SourceType))]
unknownVars) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply)) forall a b. (a -> b) -> a -> b
$ (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, (Text, SourceType))]
unknownVars) forall a. Semigroup a => a -> a -> a
<> (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall (a :: ProperNameType). ProperName a -> Text
runProperName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ProperName 'TypeName, SourceType)]
freeVarsDict)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Constraint SourceAnn]
allConstraints, [SourceType]
allKinds, [SourceType]
allArgs, [(Text, SourceType)]
varKinds)
checkKindDeclaration
:: forall m. (MonadSupply m, MonadError MultipleErrors m, MonadState CheckState m)
=> ModuleName
-> SourceType
-> m SourceType
checkKindDeclaration :: forall (m :: * -> *).
(MonadSupply m, MonadError MultipleErrors m,
MonadState CheckState m) =>
ModuleName -> SourceType -> m SourceType
checkKindDeclaration ModuleName
_ SourceType
ty = do
(SourceType
ty', SourceType
kind) <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m (SourceType, SourceType)
kindOf SourceType
ty
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
checkTypeKind SourceType
kind SourceType
E.kindType
SourceType
ty'' <- forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms SourceType
ty'
[(Int, SourceType)]
unks <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
[Int] -> m [(Int, SourceType)]
unknownsWithKinds forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IS.toList forall a b. (a -> b) -> a -> b
$ forall a. Type a -> IntSet
unknowns SourceType
ty''
SourceType
finalTy <- [(Int, SourceType)] -> SourceType -> SourceType
generalizeUnknowns [(Int, SourceType)]
unks forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {a} {a}. Type a -> Type a -> m (Type a)
freshenForAlls SourceType
ty' SourceType
ty''
forall (m :: * -> *).
MonadError MultipleErrors m =>
SourceType -> m ()
checkQuantification SourceType
finalTy
SourceType -> m SourceType
checkValidKind SourceType
finalTy
where
freshVar :: Text -> f Text
freshVar Text
arg = (Text
arg forall a. Semigroup a => a -> a -> a
<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadSupply m => m Integer
fresh
freshenForAlls :: Type a -> Type a -> m (Type a)
freshenForAlls = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
(ForAll a
_ TypeVarVisibility
_ Text
v1 Maybe (Type a)
_ Type a
ty1 Maybe SkolemScope
_, ForAll a
a2 TypeVarVisibility
vis Text
v2 Maybe (Type a)
k2 Type a
ty2 Maybe SkolemScope
sc2) | Text
v1 forall a. Eq a => a -> a -> Bool
== Text
v2 -> do
Type a
ty2' <- Type a -> Type a -> m (Type a)
freshenForAlls Type a
ty1 Type a
ty2
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a.
a
-> TypeVarVisibility
-> Text
-> Maybe (Type a)
-> Type a
-> Maybe SkolemScope
-> Type a
ForAll a
a2 TypeVarVisibility
vis Text
v2 Maybe (Type a)
k2 Type a
ty2' Maybe SkolemScope
sc2
(Type a
_, Type a
ty2) -> forall {a}. Type a -> m (Type a)
go Type a
ty2 where
go :: Type a -> m (Type a)
go = \case
ForAll a
a' TypeVarVisibility
vis Text
v' Maybe (Type a)
k' Type a
ty' Maybe SkolemScope
sc' -> do
Text
v'' <- forall {f :: * -> *}. MonadSupply f => Text -> f Text
freshVar Text
v'
Type a
ty'' <- Type a -> m (Type a)
go (forall a. Text -> Type a -> Type a -> Type a
replaceTypeVars Text
v' (forall a. a -> Text -> Type a
TypeVar a
a' Text
v'') Type a
ty')
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a.
a
-> TypeVarVisibility
-> Text
-> Maybe (Type a)
-> Type a
-> Maybe SkolemScope
-> Type a
ForAll a
a' TypeVarVisibility
vis Text
v'' Maybe (Type a)
k' Type a
ty'' Maybe SkolemScope
sc'
Type a
other -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Type a
other
checkValidKind :: SourceType -> m SourceType
checkValidKind = forall (m :: * -> *) a.
Monad m =>
(Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereOnTypesM forall a b. (a -> b) -> a -> b
$ \case
ty' :: SourceType
ty'@(ConstrainedType SourceAnn
ann Constraint SourceAnn
_ SourceType
_) ->
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' (forall a b. (a, b) -> a
fst SourceAnn
ann) forall a b. (a -> b) -> a -> b
$ SourceType -> SimpleErrorMessage
UnsupportedTypeInKind SourceType
ty'
SourceType
other -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
other
existingSignatureOrFreshKind
:: forall m. MonadState CheckState m
=> ModuleName
-> SourceSpan
-> ProperName 'TypeName
-> m SourceType
existingSignatureOrFreshKind :: forall (m :: * -> *).
MonadState CheckState m =>
ModuleName -> SourceSpan -> ProperName 'TypeName -> m SourceType
existingSignatureOrFreshKind ModuleName
moduleName SourceSpan
ss ProperName 'TypeName
name = do
Environment
env <- forall (m :: * -> *). MonadState CheckState m => m Environment
getEnv
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall a. QualifiedBy -> a -> Qualified a
Qualified (ModuleName -> QualifiedBy
ByModuleName ModuleName
moduleName) ProperName 'TypeName
name) (Environment
-> Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
E.types Environment
env) of
Maybe (SourceType, TypeKind)
Nothing -> forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind SourceSpan
ss
Just (SourceType
kind, TypeKind
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
kind
kindsOfAll
:: forall m. (MonadError MultipleErrors m, MonadState CheckState m)
=> ModuleName
-> [TypeDeclarationArgs]
-> [DataDeclarationArgs]
-> [ClassDeclarationArgs]
-> m ([TypeDeclarationResult], [DataDeclarationResult], [ClassDeclarationResult])
kindsOfAll :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModuleName
-> [TypeDeclarationArgs]
-> [DataDeclarationArgs]
-> [ClassDeclarationArgs]
-> m ([(SourceType, SourceType)], [DataDeclarationResult],
[ClassDeclarationResult])
kindsOfAll ModuleName
moduleName [TypeDeclarationArgs]
syns [DataDeclarationArgs]
dats [ClassDeclarationArgs]
clss = forall (m :: * -> *) a. MonadState CheckState m => m a -> m a
withFreshSubstitution forall a b. (a -> b) -> a -> b
$ do
[(ProperName 'TypeName, SourceType)]
synDict <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [TypeDeclarationArgs]
syns forall a b. (a -> b) -> a -> b
$ \(SourceAnn
sa, ProperName 'TypeName
synName, [(Text, Maybe SourceType)]
_, SourceType
_) -> (ProperName 'TypeName
synName,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
ModuleName -> SourceSpan -> ProperName 'TypeName -> m SourceType
existingSignatureOrFreshKind ModuleName
moduleName (forall a b. (a, b) -> a
fst SourceAnn
sa) ProperName 'TypeName
synName
[(ProperName 'TypeName, SourceType)]
datDict <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [DataDeclarationArgs]
dats forall a b. (a -> b) -> a -> b
$ \(SourceAnn
sa, ProperName 'TypeName
datName, [(Text, Maybe SourceType)]
_, [DataConstructorDeclaration]
_) -> (ProperName 'TypeName
datName,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
ModuleName -> SourceSpan -> ProperName 'TypeName -> m SourceType
existingSignatureOrFreshKind ModuleName
moduleName (forall a b. (a, b) -> a
fst SourceAnn
sa) ProperName 'TypeName
datName
[(ProperName 'TypeName, SourceType)]
clsDict <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [ClassDeclarationArgs]
clss forall a b. (a -> b) -> a -> b
$ \(SourceAnn
sa, ProperName 'ClassName
clsName, [(Text, Maybe SourceType)]
_, [Constraint SourceAnn]
_, [Declaration]
_) -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a -> ProperName b
coerceProperName ProperName 'ClassName
clsName,) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadState CheckState m =>
ModuleName -> SourceSpan -> ProperName 'TypeName -> m SourceType
existingSignatureOrFreshKind ModuleName
moduleName (forall a b. (a, b) -> a
fst SourceAnn
sa) forall a b. (a -> b) -> a -> b
$ forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a -> ProperName b
coerceProperName ProperName 'ClassName
clsName
let bindingGroup :: [(ProperName 'TypeName, SourceType)]
bindingGroup = [(ProperName 'TypeName, SourceType)]
synDict forall a. Semigroup a => a -> a -> a
<> [(ProperName 'TypeName, SourceType)]
datDict forall a. Semigroup a => a -> a -> a
<> [(ProperName 'TypeName, SourceType)]
clsDict
forall (m :: * -> *) a.
MonadState CheckState m =>
ModuleName -> [(ProperName 'TypeName, SourceType)] -> m a -> m a
bindLocalTypeVariables ModuleName
moduleName [(ProperName 'TypeName, SourceType)]
bindingGroup forall a b. (a -> b) -> a -> b
$ do
[SourceType]
synResults <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [TypeDeclarationArgs]
syns (forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModuleName -> TypeDeclarationArgs -> m SourceType
inferTypeSynonym ModuleName
moduleName)
[[(DataConstructorDeclaration, SourceType)]]
datResults <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [DataDeclarationArgs]
dats (forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModuleName
-> DataDeclarationArgs
-> m [(DataConstructorDeclaration, SourceType)]
inferDataDeclaration ModuleName
moduleName)
[([(Text, SourceType)], [Constraint SourceAnn], [Declaration])]
clsResults <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [ClassDeclarationArgs]
clss (forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModuleName
-> ClassDeclarationArgs
-> m ([(Text, SourceType)], [Constraint SourceAnn], [Declaration])
inferClassDeclaration ModuleName
moduleName)
[(((ProperName 'TypeName, SourceType), SourceType), IntSet)]
synResultsWithUnks <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (forall a b. [a] -> [b] -> [(a, b)]
zip [(ProperName 'TypeName, SourceType)]
synDict [SourceType]
synResults) forall a b. (a -> b) -> a -> b
$ \((ProperName 'TypeName
synName, SourceType
synKind), SourceType
synBody) -> do
SourceType
synKind' <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
synKind
SourceType
synBody' <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
synBody
forall (f :: * -> *) a. Applicative f => a -> f a
pure (((ProperName 'TypeName
synName, SourceType
synKind'), SourceType
synBody'), forall a. Type a -> IntSet
unknowns SourceType
synKind')
[(((ProperName 'TypeName, SourceType),
[(DataConstructorDeclaration, SourceType)]),
IntSet)]
datResultsWithUnks <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (forall a b. [a] -> [b] -> [(a, b)]
zip [(ProperName 'TypeName, SourceType)]
datDict [[(DataConstructorDeclaration, SourceType)]]
datResults) forall a b. (a -> b) -> a -> b
$ \((ProperName 'TypeName
datName, SourceType
datKind), [(DataConstructorDeclaration, SourceType)]
ctors) -> do
SourceType
datKind' <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
datKind
[(DataConstructorDeclaration, SourceType)]
ctors' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse (forall (m :: * -> *).
Monad m =>
([(Ident, SourceType)] -> m [(Ident, SourceType)])
-> DataConstructorDeclaration -> m DataConstructorDeclaration
traverseDataCtorFields (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply))) forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply) [(DataConstructorDeclaration, SourceType)]
ctors
forall (f :: * -> *) a. Applicative f => a -> f a
pure (((ProperName 'TypeName
datName, SourceType
datKind'), [(DataConstructorDeclaration, SourceType)]
ctors'), forall a. Type a -> IntSet
unknowns SourceType
datKind')
[(((ProperName 'TypeName, SourceType),
([(Text, SourceType)], [Constraint SourceAnn], [Declaration])),
IntSet)]
clsResultsWithUnks <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (forall a b. [a] -> [b] -> [(a, b)]
zip [(ProperName 'TypeName, SourceType)]
clsDict [([(Text, SourceType)], [Constraint SourceAnn], [Declaration])]
clsResults) forall a b. (a -> b) -> a -> b
$ \((ProperName 'TypeName
clsName, SourceType
clsKind), ([(Text, SourceType)]
args, [Constraint SourceAnn]
supers, [Declaration]
decls)) -> do
SourceType
clsKind' <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
clsKind
[(Text, SourceType)]
args' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply) [(Text, SourceType)]
args
[Constraint SourceAnn]
supers' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Constraint SourceAnn -> m (Constraint SourceAnn)
applyConstraint [Constraint SourceAnn]
supers
[Declaration]
decls' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Declaration -> m Declaration
applyClassMemberDeclaration [Declaration]
decls
forall (f :: * -> *) a. Applicative f => a -> f a
pure (((ProperName 'TypeName
clsName, SourceType
clsKind'), ([(Text, SourceType)]
args', [Constraint SourceAnn]
supers', [Declaration]
decls')), forall a. Type a -> IntSet
unknowns SourceType
clsKind')
let synUnks :: [(ProperName 'TypeName, IntSet)]
synUnks = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(((ProperName 'TypeName
synName, SourceType
_), SourceType
_), IntSet
unks) -> (ProperName 'TypeName
synName, IntSet
unks)) [(((ProperName 'TypeName, SourceType), SourceType), IntSet)]
synResultsWithUnks
datUnks :: [(ProperName 'TypeName, IntSet)]
datUnks = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(((ProperName 'TypeName
datName, SourceType
_), [(DataConstructorDeclaration, SourceType)]
_), IntSet
unks) -> (ProperName 'TypeName
datName, IntSet
unks)) [(((ProperName 'TypeName, SourceType),
[(DataConstructorDeclaration, SourceType)]),
IntSet)]
datResultsWithUnks
clsUnks :: [(ProperName 'TypeName, IntSet)]
clsUnks = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(((ProperName 'TypeName
clsName, SourceType
_), ([(Text, SourceType)], [Constraint SourceAnn], [Declaration])
_), IntSet
unks) -> (ProperName 'TypeName
clsName, IntSet
unks)) [(((ProperName 'TypeName, SourceType),
([(Text, SourceType)], [Constraint SourceAnn], [Declaration])),
IntSet)]
clsResultsWithUnks
tysUnks :: [(ProperName 'TypeName, IntSet)]
tysUnks = [(ProperName 'TypeName, IntSet)]
synUnks forall a. Semigroup a => a -> a -> a
<> [(ProperName 'TypeName, IntSet)]
datUnks forall a. Semigroup a => a -> a -> a
<> [(ProperName 'TypeName, IntSet)]
clsUnks
[(Int, SourceType)]
allUnks <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
HasCallStack) =>
[Int] -> m [(Int, SourceType)]
unknownsWithKinds forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IS.toList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a b. (a, b) -> b
snd [(ProperName 'TypeName, IntSet)]
tysUnks
let mkTySub :: (ProperName 'TypeName, IntSet)
-> (Qualified (ProperName 'TypeName),
(SourceType, [(Int, SourceType)]))
mkTySub (ProperName 'TypeName
name, IntSet
unks) = do
let tyCtorName :: Qualified (ProperName 'TypeName)
tyCtorName = forall a. a -> ModuleName -> Qualified a
mkQualified ProperName 'TypeName
name ModuleName
moduleName
tyUnks :: [(Int, SourceType)]
tyUnks = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> IntSet -> Bool
IS.member IntSet
unks forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Int, SourceType)]
allUnks
tyCtor :: SourceType
tyCtor = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\SourceType
ty -> SourceType -> SourceType -> SourceType
srcKindApp SourceType
ty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Int -> Type a
TUnknown SourceAnn
nullSourceAnn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) (Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
tyCtorName) [(Int, SourceType)]
tyUnks
(Qualified (ProperName 'TypeName)
tyCtorName, (SourceType
tyCtor, [(Int, SourceType)]
tyUnks))
tySubs :: [(Qualified (ProperName 'TypeName),
(SourceType, [(Int, SourceType)]))]
tySubs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ProperName 'TypeName, IntSet)
-> (Qualified (ProperName 'TypeName),
(SourceType, [(Int, SourceType)]))
mkTySub [(ProperName 'TypeName, IntSet)]
tysUnks
replaceTypeCtors :: SourceType -> SourceType
replaceTypeCtors = forall a. (Type a -> Type a) -> Type a -> Type a
everywhereOnTypes forall a b. (a -> b) -> a -> b
$ \case
TypeConstructor SourceAnn
_ Qualified (ProperName 'TypeName)
name
| Just (SourceType
tyCtor, [(Int, SourceType)]
_) <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Qualified (ProperName 'TypeName)
name [(Qualified (ProperName 'TypeName),
(SourceType, [(Int, SourceType)]))]
tySubs -> SourceType
tyCtor
SourceType
other -> SourceType
other
clsResultsWithKinds :: [ClassDeclarationResult]
clsResultsWithKinds = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(((ProperName 'TypeName, SourceType),
([(Text, SourceType)], [Constraint SourceAnn], [Declaration])),
IntSet)]
clsResultsWithUnks forall a b. (a -> b) -> a -> b
$ \(((ProperName 'TypeName
clsName, SourceType
clsKind), ([(Text, SourceType)]
args, [Constraint SourceAnn]
supers, [Declaration]
decls)), IntSet
_) -> do
let tyUnks :: [(Int, SourceType)]
tyUnks = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (forall a. a -> ModuleName -> Qualified a
mkQualified ProperName 'TypeName
clsName ModuleName
moduleName) [(Qualified (ProperName 'TypeName),
(SourceType, [(Int, SourceType)]))]
tySubs
(Declaration -> [Text]
usedTypeVariablesInDecls, Expr -> [Text]
_, Binder -> [Text]
_, CaseAlternative -> [Text]
_, DoNotationElement -> [Text]
_) = forall r.
Monoid r =>
(SourceType -> r)
-> (Declaration -> r, Expr -> r, Binder -> r, CaseAlternative -> r,
DoNotationElement -> r)
accumTypes forall a. Type a -> [Text]
usedTypeVariables
usedVars :: [Text]
usedVars = forall a. Type a -> [Text]
usedTypeVariables SourceType
clsKind
forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a. Type a -> [Text]
usedTypeVariables forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Text, SourceType)]
args
forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. Type a -> [Text]
usedTypeVariables forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\Constraint SourceAnn
c -> forall a. Constraint a -> [Type a]
constraintKindArgs Constraint SourceAnn
c forall a. Semigroup a => a -> a -> a
<> forall a. Constraint a -> [Type a]
constraintArgs Constraint SourceAnn
c)) [Constraint SourceAnn]
supers
forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Declaration -> [Text]
usedTypeVariablesInDecls [Declaration]
decls
unkBinders :: [(Int, (Text, SourceType))]
unkBinders = [Text] -> [(Int, SourceType)] -> [(Int, (Text, SourceType))]
unknownVarNames [Text]
usedVars [(Int, SourceType)]
tyUnks
args' :: [(Text, SourceType)]
args' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. [(Int, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars [(Int, (Text, SourceType))]
unkBinders forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceType -> SourceType
replaceTypeCtors) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, SourceType)]
args
supers' :: [Constraint SourceAnn]
supers' = forall a. ([Type a] -> [Type a]) -> Constraint a -> Constraint a
mapConstraintArgsAll (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. [(Int, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars [(Int, (Text, SourceType))]
unkBinders forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceType -> SourceType
replaceTypeCtors)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Constraint SourceAnn]
supers
decls' :: [Declaration]
decls' = (SourceType -> SourceType) -> Declaration -> Declaration
mapTypeDeclaration (forall a. [(Int, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars [(Int, (Text, SourceType))]
unkBinders forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceType -> SourceType
replaceTypeCtors) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Declaration]
decls
([(Text, SourceType)]
args', [Constraint SourceAnn]
supers', [Declaration]
decls', [(Int, (Text, SourceType))] -> SourceType -> SourceType
generalizeUnknownsWithVars [(Int, (Text, SourceType))]
unkBinders SourceType
clsKind)
[DataDeclarationResult]
datResultsWithKinds <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(((ProperName 'TypeName, SourceType),
[(DataConstructorDeclaration, SourceType)]),
IntSet)]
datResultsWithUnks forall a b. (a -> b) -> a -> b
$ \(((ProperName 'TypeName
datName, SourceType
datKind), [(DataConstructorDeclaration, SourceType)]
ctors), IntSet
_) -> do
let tyUnks :: [(Int, SourceType)]
tyUnks = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (forall a. a -> ModuleName -> Qualified a
mkQualified ProperName 'TypeName
datName ModuleName
moduleName) [(Qualified (ProperName 'TypeName),
(SourceType, [(Int, SourceType)]))]
tySubs
replaceDataCtorField :: SourceType -> SourceType
replaceDataCtorField SourceType
ty = forall a. [(Int, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars ([Text] -> [(Int, SourceType)] -> [(Int, (Text, SourceType))]
unknownVarNames (forall a. Type a -> [Text]
usedTypeVariables SourceType
ty) [(Int, SourceType)]
tyUnks) forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType
replaceTypeCtors SourceType
ty
ctors' :: [(DataConstructorDeclaration, SourceType)]
ctors' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([(Ident, SourceType)] -> [(Ident, SourceType)])
-> DataConstructorDeclaration -> DataConstructorDeclaration
mapDataCtorFields (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SourceType -> SourceType
replaceDataCtorField)) forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [(Int, SourceType)] -> SourceType -> SourceType
generalizeUnknowns [(Int, SourceType)]
tyUnks forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceType -> SourceType
replaceTypeCtors) [(DataConstructorDeclaration, SourceType)]
ctors
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ forall (m :: * -> *).
MonadError MultipleErrors m =>
SourceType -> m ()
checkTypeQuantification) [(DataConstructorDeclaration, SourceType)]
ctors'
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(DataConstructorDeclaration, SourceType)]
ctors', [(Int, SourceType)] -> SourceType -> SourceType
generalizeUnknowns [(Int, SourceType)]
tyUnks SourceType
datKind)
[(SourceType, SourceType)]
synResultsWithKinds <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(((ProperName 'TypeName, SourceType), SourceType), IntSet)]
synResultsWithUnks forall a b. (a -> b) -> a -> b
$ \(((ProperName 'TypeName
synName, SourceType
synKind), SourceType
synBody), IntSet
_) -> do
let tyUnks :: [(Int, SourceType)]
tyUnks = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (forall a. a -> ModuleName -> Qualified a
mkQualified ProperName 'TypeName
synName ModuleName
moduleName) [(Qualified (ProperName 'TypeName),
(SourceType, [(Int, SourceType)]))]
tySubs
unkBinders :: [(Int, (Text, SourceType))]
unkBinders = [Text] -> [(Int, SourceType)] -> [(Int, (Text, SourceType))]
unknownVarNames (forall a. Type a -> [Text]
usedTypeVariables SourceType
synKind forall a. Semigroup a => a -> a -> a
<> forall a. Type a -> [Text]
usedTypeVariables SourceType
synBody) [(Int, SourceType)]
tyUnks
genBody :: SourceType
genBody = forall a. [(Int, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars [(Int, (Text, SourceType))]
unkBinders forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType
replaceTypeCtors SourceType
synBody
genSig :: SourceType
genSig = [(Int, (Text, SourceType))] -> SourceType -> SourceType
generalizeUnknownsWithVars [(Int, (Text, SourceType))]
unkBinders SourceType
synKind
forall (m :: * -> *).
MonadError MultipleErrors m =>
SourceType -> m ()
checkEscapedSkolems SourceType
genBody
forall (m :: * -> *).
MonadError MultipleErrors m =>
SourceType -> m ()
checkTypeQuantification SourceType
genBody
forall (m :: * -> *).
MonadError MultipleErrors m =>
SourceType -> m ()
checkVisibleTypeQuantification SourceType
genSig
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
genBody, SourceType
genSig)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(SourceType, SourceType)]
synResultsWithKinds, [DataDeclarationResult]
datResultsWithKinds, [ClassDeclarationResult]
clsResultsWithKinds)