-- |
-- This module implements the kind checker
--
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 t` is identical to `checkKind t E.kindType` except
-- that the former checks that the type synonyms in `t` expand completely. This
-- is the appropriate function to use when expanding the types of type
-- parameter kinds, arguments to data constructors, etc., in order for the
-- PartiallyAppliedSynonym error to take precedence over the KindsDoNotUnify
-- error.
--
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

-- | Does not attach positions to the error node, instead relies on the
-- | local position context. This is useful when invoking kind unification
-- | outside of kind checker internals.
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

-- | Check the kind of a type, failing if it is not of kind *.
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
      -- Normally we wouldn't unify in `elaborateKind`, since an unknown should
      -- always have a known kind. However, since type holes are fully inference
      -- driven, they are unknowns with unknown kinds, which may require some
      -- late unification here.
      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)

-- | Infer the kind of a single type
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

-- | Infer the kind of a single type, returning the kinds of any scoped type variables
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)]
  -- The infered type signatures of data constructors
  , SourceType
  -- The inferred kind of the declaration
  )

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
  -- The elaborated rhs of the declaration
  , SourceType
  -- The inferred kind of the declaration
  )

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

-- | Checks that a particular generalization is valid and well-scoped.
-- | Implicitly generalized kinds are always elaborated before explicitly
-- | quantified type variables. It's possible that such a kind can be
-- | inserted before other variables that it depends on, making it
-- | ill-scoped. We require that users explicitly generalize this kind
-- | in such a case.
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

-- | Checks that there are no remaining unknowns in a type, and if so
-- | throws an error. This is necessary for contexts where we can't
-- | implicitly generalize unknowns, such as on the right-hand-side of
-- | a type synonym, or in arguments to data constructors.
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)]
  -- The kind annotated class arguments
  , [SourceConstraint]
  -- The kind annotated superclass constraints
  , [Declaration]
  -- The kind annotated declarations
  , SourceType
  -- The inferred kind of the declaration
  )

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
  -- When expanding type synonyms and generalizing, we need to generate more
  -- unique names so that they don't clash or shadow other names, or can
  -- be referenced (easily).
  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)