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
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State
import Control.Monad.Supply.Class
import Data.Bifunctor (first)
import Data.Bitraversable (bitraverse)
import Data.Foldable (for_, traverse_)
import Data.Function (on)
import Data.Functor (($>))
import qualified Data.IntSet as IS
import Data.List (nubBy, sortOn, (\\))
import qualified Data.Map as M
import Data.Maybe (fromJust, fromMaybe)
import Data.Text (Text)
import qualified Data.Text as T
import Data.Traversable (for)
import Language.PureScript.Crash
import qualified Language.PureScript.Environment as E
import Language.PureScript.Errors
import Language.PureScript.Names
import Language.PureScript.TypeChecker.Monad
import Language.PureScript.TypeChecker.Skolems (newSkolemConstant, newSkolemScope, skolemize)
import Language.PureScript.TypeChecker.Synonyms
import Language.PureScript.Types
import Language.PureScript.Pretty.Types
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
_ 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 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
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll SourceAnn
ann 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
_ 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
_ 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
_ 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 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 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
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.
(Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith SourceType -> SourceType -> m ()
go 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
_ 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 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'
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. [(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 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
_ Text
v1 Maybe (Type a)
_ Type a
ty1 Maybe SkolemScope
_, ForAll a
a2 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
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
a2 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' 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
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
a' 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)