-- |
-- 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 (join, unless, void, when, (<=<))
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State (MonadState, gets, modify)
import Control.Monad.Supply.Class (MonadSupply(..))

import Data.Bifunctor (first)
import Data.Bitraversable (bitraverse)
import Data.Foldable (for_, traverse_)
import Data.Function (on)
import Data.Functor (($>))
import Data.IntSet qualified as IS
import Data.List (nubBy, sortOn, (\\))
import Data.Map qualified as M
import Data.Maybe (fromJust, fromMaybe)
import Data.Text (Text)
import Data.Text qualified as T
import Data.Traversable (for)

import Language.PureScript.Crash (HasCallStack, internalError)
import Language.PureScript.Environment qualified as E
import Language.PureScript.Errors
import Language.PureScript.Names (pattern ByNullSourcePos, ModuleName, Name(..), ProperName(..), ProperNameType(..), Qualified(..), QualifiedBy(..), coerceProperName, mkQualified)
import Language.PureScript.TypeChecker.Monad (CheckState(..), Substitution(..), UnkLevel(..), Unknown, bindLocalTypeVariables, debugType, getEnv, lookupTypeVariable, unsafeCheckCurrentModule, withErrorMessageHint, withFreshSubstitution)
import Language.PureScript.TypeChecker.Skolems (newSkolemConstant, newSkolemScope, skolemize)
import Language.PureScript.TypeChecker.Synonyms (replaceAllTypeSynonyms)
import Language.PureScript.Types
import Language.PureScript.Pretty.Types (prettyPrintType)

generalizeUnknowns :: [(Unknown, SourceType)] -> SourceType -> SourceType
generalizeUnknowns :: [(Int, SourceType)] -> SourceType -> SourceType
generalizeUnknowns [(Int, SourceType)]
unks SourceType
ty =
  [(Int, (Text, SourceType))] -> SourceType -> SourceType
generalizeUnknownsWithVars ([Text] -> [(Int, SourceType)] -> [(Int, (Text, SourceType))]
unknownVarNames (forall a. Type a -> [Text]
usedTypeVariables SourceType
ty) [(Int, SourceType)]
unks) SourceType
ty

generalizeUnknownsWithVars :: [(Unknown, (Text, SourceType))] -> SourceType -> SourceType
generalizeUnknownsWithVars :: [(Int, (Text, SourceType))] -> SourceType -> SourceType
generalizeUnknownsWithVars [(Int, (Text, SourceType))]
binders SourceType
ty =
  forall a. [(a, (Text, Maybe (Type a)))] -> Type a -> Type a
mkForAll ((forall a. Type a -> a
getAnnForType SourceType
ty,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [(Int, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars [(Int, (Text, SourceType))]
binders) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, (Text, SourceType))]
binders) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [(Int, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars [(Int, (Text, SourceType))]
binders forall a b. (a -> b) -> a -> b
$ SourceType
ty

replaceUnknownsWithVars :: [(Unknown, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars :: forall a. [(Int, (Text, a))] -> SourceType -> SourceType
replaceUnknownsWithVars [(Int, (Text, a))]
binders SourceType
ty
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, (Text, a))]
binders = SourceType
ty
  | Bool
otherwise = SourceType -> SourceType
go SourceType
ty
  where
  go :: SourceType -> SourceType
  go :: SourceType -> SourceType
go = forall a. (Type a -> Type a) -> Type a -> Type a
everywhereOnTypes forall a b. (a -> b) -> a -> b
$ \case
    TUnknown SourceAnn
ann Int
unk | Just (Text
name, a
_) <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
unk [(Int, (Text, a))]
binders -> forall a. a -> Text -> Type a
TypeVar SourceAnn
ann Text
name
    SourceType
other -> SourceType
other

unknownVarNames :: [Text] -> [(Unknown, SourceType)] -> [(Unknown, (Text, SourceType))]
unknownVarNames :: [Text] -> [(Int, SourceType)] -> [(Int, (Text, SourceType))]
unknownVarNames [Text]
used [(Int, SourceType)]
unks =
  forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Int
a, SourceType
b) Text
n -> (Int
a, (Text
n, SourceType
b))) [(Int, SourceType)]
unks forall a b. (a -> b) -> a -> b
$ [Text]
allVars forall a. Eq a => [a] -> [a] -> [a]
\\ [Text]
used
  where
  allVars :: [Text]
  allVars :: [Text]
allVars
    | [(Int, SourceType)
_] <- [(Int, SourceType)]
unks = Text
"k" forall a. a -> [a] -> [a]
: [Text]
vars
    | Bool
otherwise = [Text]
vars

  vars :: [Text]
  vars :: [Text]
vars = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Text
"k" forall a. Semigroup a => a -> a -> a
<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) ([Int
1..] :: [Int])

apply :: (MonadState CheckState m) => SourceType -> m SourceType
apply :: forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
ty = forall a b c. (a -> b -> c) -> b -> a -> c
flip Substitution -> SourceType -> SourceType
substituteType SourceType
ty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Substitution
checkSubstitution

substituteType :: Substitution -> SourceType -> SourceType
substituteType :: Substitution -> SourceType -> SourceType
substituteType Substitution
sub = forall a. (Type a -> Type a) -> Type a -> Type a
everywhereOnTypes forall a b. (a -> b) -> a -> b
$ \case
  TUnknown SourceAnn
ann Int
u ->
    case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
u (Substitution -> Map Int SourceType
substType Substitution
sub) of
      Maybe SourceType
Nothing -> forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u
      Just (TUnknown SourceAnn
ann' Int
u1) | Int
u1 forall a. Eq a => a -> a -> Bool
== Int
u -> forall a. a -> Int -> Type a
TUnknown SourceAnn
ann' Int
u1
      Just SourceType
t -> Substitution -> SourceType -> SourceType
substituteType Substitution
sub SourceType
t
  SourceType
other ->
    SourceType
other

freshUnknown :: (MonadState CheckState m) => m Unknown
freshUnknown :: forall (m :: * -> *). MonadState CheckState m => m Int
freshUnknown = do
  Int
k <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Int
checkNextType
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CheckState
st -> CheckState
st { checkNextType :: Int
checkNextType = Int
k forall a. Num a => a -> a -> a
+ Int
1 }
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
k

freshKind :: (MonadState CheckState m) => SourceSpan -> m SourceType
freshKind :: forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind SourceSpan
ss = forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> SourceType -> m SourceType
freshKindWithKind SourceSpan
ss SourceType
E.kindType

freshKindWithKind :: (MonadState CheckState m) => SourceSpan -> SourceType -> m SourceType
freshKindWithKind :: forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> SourceType -> m SourceType
freshKindWithKind SourceSpan
ss SourceType
kind = do
  Int
u <- forall (m :: * -> *). MonadState CheckState m => m Int
freshUnknown
  forall (m :: * -> *).
MonadState CheckState m =>
Maybe UnkLevel -> Int -> SourceType -> m ()
addUnsolved forall a. Maybe a
Nothing Int
u SourceType
kind
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Int -> Type a
TUnknown (SourceSpan
ss, []) Int
u

addUnsolved :: (MonadState CheckState m) => Maybe UnkLevel -> Unknown -> SourceType -> m ()
addUnsolved :: forall (m :: * -> *).
MonadState CheckState m =>
Maybe UnkLevel -> Int -> SourceType -> m ()
addUnsolved Maybe UnkLevel
lvl Int
unk SourceType
kind = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CheckState
st -> do
  let
    newLvl :: UnkLevel
newLvl = NonEmpty Int -> UnkLevel
UnkLevel forall a b. (a -> b) -> a -> b
$ case Maybe UnkLevel
lvl of
      Maybe UnkLevel
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
unk
      Just (UnkLevel NonEmpty Int
lvl') -> NonEmpty Int
lvl' forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
unk
    subs :: Substitution
subs = CheckState -> Substitution
checkSubstitution CheckState
st
    uns :: Map Int (UnkLevel, SourceType)
uns = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
unk (UnkLevel
newLvl, SourceType
kind) forall a b. (a -> b) -> a -> b
$ Substitution -> Map Int (UnkLevel, SourceType)
substUnsolved Substitution
subs
  CheckState
st { checkSubstitution :: Substitution
checkSubstitution = Substitution
subs { substUnsolved :: Map Int (UnkLevel, SourceType)
substUnsolved = Map Int (UnkLevel, SourceType)
uns } }

solve :: (MonadState CheckState m) => Unknown -> SourceType -> m ()
solve :: forall (m :: * -> *).
MonadState CheckState m =>
Int -> SourceType -> m ()
solve Int
unk SourceType
solution = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CheckState
st -> do
  let
    subs :: Substitution
subs = CheckState -> Substitution
checkSubstitution CheckState
st
    tys :: Map Int SourceType
tys = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
unk SourceType
solution forall a b. (a -> b) -> a -> b
$ Substitution -> Map Int SourceType
substType Substitution
subs
  CheckState
st { checkSubstitution :: Substitution
checkSubstitution = Substitution
subs { substType :: Map Int SourceType
substType = Map Int SourceType
tys } }

lookupUnsolved
  :: (MonadState CheckState m, MonadError MultipleErrors m, HasCallStack)
  => Unknown
  -> m (UnkLevel, SourceType)
lookupUnsolved :: forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
 HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
u = do
  Map Int (UnkLevel, SourceType)
uns <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Substitution -> Map Int (UnkLevel, SourceType)
substUnsolved forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckState -> Substitution
checkSubstitution)
  case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
u Map Int (UnkLevel, SourceType)
uns of
    Maybe (UnkLevel, SourceType)
Nothing -> forall (m :: * -> *) a.
(MonadError MultipleErrors m, HasCallStack) =>
Text -> m a
internalCompilerError forall a b. (a -> b) -> a -> b
$ Text
"Unsolved unification variable ?" forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (forall a. Show a => a -> String
show Int
u) forall a. Semigroup a => a -> a -> a
<> Text
" is not bound"
    Just (UnkLevel, SourceType)
res -> forall (m :: * -> *) a. Monad m => a -> m a
return (UnkLevel, SourceType)
res

unknownsWithKinds
  :: forall m. (MonadState CheckState m, MonadError MultipleErrors m, HasCallStack)
  => [Unknown]
  -> m [(Unknown, SourceType)]
unknownsWithKinds :: forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
 HasCallStack) =>
[Int] -> m [(Int, SourceType)]
unknownsWithKinds = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => m (m a) -> m a
join) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall {m :: * -> *}.
(MonadState CheckState m, MonadError MultipleErrors m) =>
Int -> m [(UnkLevel, (Int, SourceType))]
go
  where
  go :: Int -> m [(UnkLevel, (Int, SourceType))]
go Int
u = do
    (UnkLevel
lvl, SourceType
ty) <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
 HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
u
    [(UnkLevel, (Int, SourceType))]
rest <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Int -> m [(UnkLevel, (Int, SourceType))]
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IS.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> IntSet
unknowns forall a b. (a -> b) -> a -> b
$ SourceType
ty
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (UnkLevel
lvl, (Int
u, SourceType
ty)) forall a. a -> [a] -> [a]
: [(UnkLevel, (Int, SourceType))]
rest

inferKind
  :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
  => SourceType
  -> m (SourceType, SourceType)
inferKind :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> m (SourceType, SourceType)
inferKind = \SourceType
tyToInfer ->
  forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint (SourceType -> ErrorMessageHint
ErrorInferringKind SourceType
tyToInfer)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
MonadError MultipleErrors m =>
SourceSpan -> m a -> m a
rethrowWithPosition (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. Type a -> a
getAnnForType SourceType
tyToInfer)
    forall a b. (a -> b) -> a -> b
$ SourceType -> m (SourceType, SourceType)
go SourceType
tyToInfer
  where
  go :: SourceType -> m (SourceType, SourceType)
go = \case
    ty :: SourceType
ty@(TypeConstructor SourceAnn
ann Qualified (ProperName 'TypeName)
v) -> do
      Environment
env <- forall (m :: * -> *). MonadState CheckState m => m Environment
getEnv
      case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'TypeName)
v (Environment
-> Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
E.types Environment
env) of
        Maybe (SourceType, TypeKind)
Nothing ->
          forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' (forall a b. (a, b) -> a
fst SourceAnn
ann) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Qualified Name -> SimpleErrorMessage
UnknownName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProperName 'TypeName -> Name
TyName forall a b. (a -> b) -> a -> b
$ Qualified (ProperName 'TypeName)
v
        Just (SourceType
kind, TypeKind
E.LocalTypeVariable) -> do
          SourceType
kind' <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
kind
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
kind' forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
        Just (SourceType
kind, TypeKind
_) -> do
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
kind forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
    ConstrainedType SourceAnn
ann' con :: Constraint SourceAnn
con@(Constraint SourceAnn
ann Qualified (ProperName 'ClassName)
v [SourceType]
_ [SourceType]
_ Maybe ConstraintData
_) SourceType
ty -> do
      Environment
env <- forall (m :: * -> *). MonadState CheckState m => m Environment
getEnv
      Constraint SourceAnn
con' <- case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a -> ProperName b
coerceProperName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualified (ProperName 'ClassName)
v) (Environment
-> Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
E.types Environment
env) of
        Maybe (SourceType, TypeKind)
Nothing ->
          forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' (forall a b. (a, b) -> a
fst SourceAnn
ann) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Qualified Name -> SimpleErrorMessage
UnknownName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProperName 'ClassName -> Name
TyClassName forall a b. (a -> b) -> a -> b
$ Qualified (ProperName 'ClassName)
v
        Just (SourceType, TypeKind)
_ ->
          forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Constraint SourceAnn -> m (Constraint SourceAnn)
checkConstraint Constraint SourceAnn
con
      SourceType
ty' <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> m SourceType
checkIsSaturatedType SourceType
ty
      Constraint SourceAnn
con'' <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Constraint SourceAnn -> m (Constraint SourceAnn)
applyConstraint Constraint SourceAnn
con'
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType SourceAnn
ann' Constraint SourceAnn
con'' SourceType
ty', SourceType
E.kindType forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann')
    ty :: SourceType
ty@(TypeLevelString SourceAnn
ann PSString
_) ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
E.kindSymbol forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
    ty :: SourceType
ty@(TypeLevelInt SourceAnn
ann Integer
_) ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
E.tyInt forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
    ty :: SourceType
ty@(TypeVar SourceAnn
ann Text
v) -> do
      ModuleName
moduleName <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
m ModuleName
unsafeCheckCurrentModule
      SourceType
kind <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
ModuleName -> Qualified (ProperName 'TypeName) -> m SourceType
lookupTypeVariable ModuleName
moduleName (forall a. QualifiedBy -> a -> Qualified a
Qualified QualifiedBy
ByNullSourcePos forall a b. (a -> b) -> a -> b
$ forall (a :: ProperNameType). Text -> ProperName a
ProperName Text
v)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
kind forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
    ty :: SourceType
ty@(Skolem SourceAnn
ann Text
_ Maybe SourceType
mbK Int
_ SkolemScope
_) -> do
      SourceType
kind <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
internalError String
"Skolem has no kind") Maybe SourceType
mbK
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
kind forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
    ty :: SourceType
ty@(TUnknown SourceAnn
ann Int
u) -> do
      SourceType
kind <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
 HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
u
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
kind forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
    ty :: SourceType
ty@(TypeWildcard SourceAnn
ann WildcardData
_) -> do
      SourceType
k <- forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind (forall a b. (a, b) -> a
fst SourceAnn
ann)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
k forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
    ty :: SourceType
ty@(REmpty SourceAnn
ann) -> do
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
ty, SourceType
E.kindOfREmpty forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
    ty :: SourceType
ty@(RCons SourceAnn
ann Label
_ SourceType
_ SourceType
_) | ([RowListItem SourceAnn]
rowList, SourceType
rowTail) <- forall a. Type a -> ([RowListItem a], Type a)
rowToList SourceType
ty -> do
      SourceType
kr <- forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind (forall a b. (a, b) -> a
fst SourceAnn
ann)
      [RowListItem SourceAnn]
rowList' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [RowListItem SourceAnn]
rowList forall a b. (a -> b) -> a -> b
$ \(RowListItem SourceAnn
a Label
lbl SourceType
t) ->
        forall a. a -> Label -> Type a -> RowListItem a
RowListItem SourceAnn
a Label
lbl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind SourceType
t SourceType
kr
      SourceType
rowTail' <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> SourceType -> m SourceType
checkKind SourceType
rowTail forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType
E.kindRow SourceType
kr
      SourceType
kr' <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
kr
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
rowList', SourceType
rowTail'), SourceType -> SourceType
E.kindRow SourceType
kr' forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
    TypeApp SourceAnn
ann SourceType
t1 SourceType
t2 -> do
      (SourceType
t1', SourceType
k1) <- SourceType -> m (SourceType, SourceType)
go SourceType
t1
      forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceAnn
-> (SourceType, SourceType)
-> SourceType
-> m (SourceType, SourceType)
inferAppKind SourceAnn
ann (SourceType
t1', SourceType
k1) SourceType
t2
    KindApp SourceAnn
ann SourceType
t1 SourceType
t2 -> do
      (SourceType
t1', SourceType
kind) <- forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SourceType -> m (SourceType, SourceType)
go SourceType
t1
      case SourceType
kind of
        ForAll SourceAnn
_ 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
  goWithLabel :: Label -> SourceType -> SourceType -> m ()
goWithLabel Label
l SourceType
t1 SourceType
t2 = forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint (Label -> ErrorMessageHint
ErrorInRowLabel Label
l) forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> m ()
go SourceType
t1 SourceType
t2
  go :: SourceType -> SourceType -> m ()
go = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
    (TypeApp SourceAnn
_ SourceType
p1 SourceType
p2, TypeApp SourceAnn
_ SourceType
p3 SourceType
p4) -> do
      SourceType -> SourceType -> m ()
go SourceType
p1 SourceType
p3
      forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> m ()
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
p2 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
p4
    (KindApp SourceAnn
_ SourceType
p1 SourceType
p2, KindApp SourceAnn
_ SourceType
p3 SourceType
p4) -> do
      SourceType -> SourceType -> m ()
go SourceType
p1 SourceType
p3
      forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> m ()
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
p2 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
p4
    (r1 :: SourceType
r1@(RCons SourceAnn
_ Label
_ SourceType
_ SourceType
_), SourceType
r2) ->
      SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2
    (SourceType
r1, r2 :: SourceType
r2@(RCons SourceAnn
_ Label
_ SourceType
_ SourceType
_)) ->
      SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2
    (r1 :: SourceType
r1@(REmpty SourceAnn
_), SourceType
r2) ->
      SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2
    (SourceType
r1, r2 :: SourceType
r2@(REmpty SourceAnn
_)) ->
      SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2
    (SourceType
w1, SourceType
w2) | forall a b. Type a -> Type b -> Bool
eqType SourceType
w1 SourceType
w2 ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    (TUnknown SourceAnn
_ Int
a', SourceType
p1) ->
      forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
Int -> SourceType -> m ()
solveUnknown Int
a' SourceType
p1
    (SourceType
p1, TUnknown SourceAnn
_ Int
a') ->
      forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
Int -> SourceType -> m ()
solveUnknown Int
a' SourceType
p1
    (SourceType
w1, SourceType
w2) ->
      SourceType -> SourceType -> m ()
onFailure SourceType
w1 SourceType
w2

  unifyRows :: SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2 = do
    let ([m ()]
matches, (([RowListItem SourceAnn], SourceType),
 ([RowListItem SourceAnn], SourceType))
rest) = forall a r.
(Label -> Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith Label -> SourceType -> SourceType -> m ()
goWithLabel SourceType
r1 SourceType
r2
    forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
matches
    (([RowListItem SourceAnn], SourceType),
 ([RowListItem SourceAnn], SourceType))
-> m ()
unifyTails (([RowListItem SourceAnn], SourceType),
 ([RowListItem SourceAnn], SourceType))
rest

  unifyTails :: (([RowListItem SourceAnn], SourceType),
 ([RowListItem SourceAnn], SourceType))
-> m ()
unifyTails = \case
    (([], TUnknown SourceAnn
_ Int
a'), ([RowListItem SourceAnn]
rs, SourceType
p1)) ->
      forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
Int -> SourceType -> m ()
solveUnknown Int
a' forall a b. (a -> b) -> a -> b
$ forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
rs, SourceType
p1)
    (([RowListItem SourceAnn]
rs, SourceType
p1), ([], TUnknown SourceAnn
_ Int
a')) ->
      forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
Int -> SourceType -> m ()
solveUnknown Int
a' forall a b. (a -> b) -> a -> b
$ forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
rs, SourceType
p1)
    (([], SourceType
w1), ([], SourceType
w2)) | forall a b. Type a -> Type b -> Bool
eqType SourceType
w1 SourceType
w2 ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    (([RowListItem SourceAnn]
rs1, TUnknown SourceAnn
_ Int
u1), ([RowListItem SourceAnn]
rs2, TUnknown SourceAnn
_ Int
u2)) | Int
u1 forall a. Eq a => a -> a -> Bool
/= Int
u2 -> do
      SourceType
rest <- forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> m SourceType
freshKind SourceSpan
nullSourceSpan
      forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
Int -> SourceType -> m ()
solveUnknown Int
u1 forall a b. (a -> b) -> a -> b
$ forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
rs2, SourceType
rest)
      forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
Int -> SourceType -> m ()
solveUnknown Int
u2 forall a b. (a -> b) -> a -> b
$ forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
rs1, SourceType
rest)
    (([RowListItem SourceAnn], SourceType)
w1, ([RowListItem SourceAnn], SourceType)
w2) ->
      SourceType -> SourceType -> m ()
onFailure (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn], SourceType)
w1) (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn], SourceType)
w2)

solveUnknown
  :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
  => Unknown
  -> SourceType
  -> m ()
solveUnknown :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
Int -> SourceType -> m ()
solveUnknown Int
a' SourceType
p1 = do
  SourceType
p2 <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
Int -> SourceType -> m SourceType
promoteKind Int
a' SourceType
p1
  SourceType
w1 <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
 HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
a'
  forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> SourceType -> m ()
unifyKinds forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
w1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> m SourceType
elaborateKind SourceType
p2
  forall (m :: * -> *).
MonadState CheckState m =>
Int -> SourceType -> m ()
solve Int
a' SourceType
p2

solveUnknownAsFunction
  :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
  => SourceAnn
  -> Unknown
  -> m SourceType
solveUnknownAsFunction :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceAnn -> Int -> m SourceType
solveUnknownAsFunction SourceAnn
ann Int
u = do
  UnkLevel
lvl <- forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
 HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
u
  Int
u1 <- forall (m :: * -> *). MonadState CheckState m => m Int
freshUnknown
  Int
u2 <- forall (m :: * -> *). MonadState CheckState m => m Int
freshUnknown
  forall (m :: * -> *).
MonadState CheckState m =>
Maybe UnkLevel -> Int -> SourceType -> m ()
addUnsolved (forall a. a -> Maybe a
Just UnkLevel
lvl) Int
u1 SourceType
E.kindType
  forall (m :: * -> *).
MonadState CheckState m =>
Maybe UnkLevel -> Int -> SourceType -> m ()
addUnsolved (forall a. a -> Maybe a
Just UnkLevel
lvl) Int
u2 SourceType
E.kindType
  let uarr :: SourceType
uarr = (forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u1 SourceType -> SourceType -> SourceType
E.-:> forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u2) forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
  forall (m :: * -> *).
MonadState CheckState m =>
Int -> SourceType -> m ()
solve Int
u SourceType
uarr
  forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
uarr

promoteKind
  :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
  => Unknown
  -> SourceType
  -> m SourceType
promoteKind :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
Int -> SourceType -> m SourceType
promoteKind Int
u2 SourceType
ty = do
  UnkLevel
lvl2 <- forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
 HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
u2
  forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) a.
Monad m =>
(Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereOnTypesM SourceType
ty forall a b. (a -> b) -> a -> b
$ \case
    ty' :: SourceType
ty'@(TUnknown SourceAnn
ann Int
u1) -> do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
u1 forall a. Eq a => a -> a -> Bool
== Int
u2) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceType -> SimpleErrorMessage
InfiniteKind forall a b. (a -> b) -> a -> b
$ SourceType
ty
      (UnkLevel
lvl1, SourceType
k) <- forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
 HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
u1
      if UnkLevel
lvl1 forall a. Ord a => a -> a -> Bool
< UnkLevel
lvl2 then
        forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
ty'
      else do
        SourceType
k'  <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
Int -> SourceType -> m SourceType
promoteKind Int
u2 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
k
        Int
u1' <- forall (m :: * -> *). MonadState CheckState m => m Int
freshUnknown
        forall (m :: * -> *).
MonadState CheckState m =>
Maybe UnkLevel -> Int -> SourceType -> m ()
addUnsolved (forall a. a -> Maybe a
Just UnkLevel
lvl2) Int
u1' SourceType
k'
        forall (m :: * -> *).
MonadState CheckState m =>
Int -> SourceType -> m ()
solve Int
u1 forall a b. (a -> b) -> a -> b
$ forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u1'
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Int -> Type a
TUnknown SourceAnn
ann Int
u1'
    SourceType
ty' ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
ty'

elaborateKind
  :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack)
  => SourceType
  -> m SourceType
elaborateKind :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> m SourceType
elaborateKind = \case
  TypeLevelString SourceAnn
ann PSString
_ ->
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType
E.kindSymbol forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
  TypeLevelInt SourceAnn
ann Integer
_ ->
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType
E.tyInt forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
  TypeConstructor SourceAnn
ann Qualified (ProperName 'TypeName)
v -> do
    Environment
env <- forall (m :: * -> *). MonadState CheckState m => m Environment
getEnv
    case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'TypeName)
v (Environment
-> Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
E.types Environment
env) of
      Maybe (SourceType, TypeKind)
Nothing ->
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' (forall a b. (a, b) -> a
fst SourceAnn
ann) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Qualified Name -> SimpleErrorMessage
UnknownName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProperName 'TypeName -> Name
TyName forall a b. (a -> b) -> a -> b
$ Qualified (ProperName 'TypeName)
v
      Just (SourceType
kind, TypeKind
_) ->
        (forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
kind
  TypeVar SourceAnn
ann Text
a -> do
    ModuleName
moduleName <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
m ModuleName
unsafeCheckCurrentModule
    SourceType
kind <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
ModuleName -> Qualified (ProperName 'TypeName) -> m SourceType
lookupTypeVariable ModuleName
moduleName (forall a. QualifiedBy -> a -> Qualified a
Qualified QualifiedBy
ByNullSourcePos forall a b. (a -> b) -> a -> b
$ forall (a :: ProperNameType). Text -> ProperName a
ProperName Text
a)
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
kind forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann)
  (Skolem SourceAnn
ann Text
_ Maybe SourceType
mbK Int
_ SkolemScope
_) -> do
    SourceType
kind <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
internalError String
"Skolem has no kind") Maybe SourceType
mbK
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType
kind forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
  TUnknown SourceAnn
ann Int
a' -> do
    SourceType
kind <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
 HasCallStack) =>
Int -> m (UnkLevel, SourceType)
lookupUnsolved Int
a'
    (forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
apply SourceType
kind
  REmpty SourceAnn
ann -> do
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType
E.kindOfREmpty forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
  RCons SourceAnn
ann Label
_ SourceType
t1 SourceType
_ -> do
    SourceType
k1 <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> m SourceType
elaborateKind SourceType
t1
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType
E.kindRow SourceType
k1 forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
  ty :: SourceType
ty@(TypeApp SourceAnn
ann SourceType
t1 SourceType
t2) -> do
    SourceType
k1 <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> m SourceType
elaborateKind SourceType
t1
    case SourceType
k1 of
      TypeApp SourceAnn
_ (TypeApp SourceAnn
_ SourceType
k SourceType
_) SourceType
w2 | forall a b. Type a -> Type b -> Bool
eqType SourceType
k SourceType
E.tyFunction -> do
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SourceType
w2 forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceAnn
ann
      -- 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)