-- |
-- Functions and instances relating to unification
--
module Language.PureScript.TypeChecker.Unify
  ( freshType
  , freshTypeWithKind
  , solveType
  , substituteType
  , unknownsInType
  , unifyTypes
  , unifyRows
  , alignRowsWith
  , replaceTypeWildcards
  , varIfUnknown
  ) where

import Prelude

import Control.Monad (forM_, void)
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State.Class (MonadState(..), gets, modify, state)
import Control.Monad.Writer.Class (MonadWriter(..))

import Data.Foldable (traverse_)
import Data.Maybe (fromMaybe)
import Data.Map qualified as M
import Data.Text qualified as T

import Language.PureScript.Crash (internalError)
import Language.PureScript.Environment qualified as E
import Language.PureScript.Errors (ErrorMessageHint(..), MultipleErrors, SimpleErrorMessage(..), SourceAnn, errorMessage, internalCompilerError, onErrorMessages, rethrow, warnWithPosition, withoutPosition)
import Language.PureScript.TypeChecker.Kinds (elaborateKind, instantiateKind, unifyKinds')
import Language.PureScript.TypeChecker.Monad (CheckState(..), Substitution(..), UnkLevel(..), Unknown, getLocalContext, guardWith, lookupUnkName, withErrorMessageHint)
import Language.PureScript.TypeChecker.Skolems (newSkolemConstant, skolemize)
import Language.PureScript.Types (Constraint(..), pattern REmptyKinded, RowListItem(..), SourceType, Type(..), WildcardData(..), alignRowsWith, everythingOnTypes, everywhereOnTypes, everywhereOnTypesM, getAnnForType, mkForAll, rowFromList, srcTUnknown)

-- | Generate a fresh type variable with an unknown kind. Avoid this if at all possible.
freshType :: (MonadState CheckState m) => m SourceType
freshType :: forall (m :: * -> *). MonadState CheckState m => m SourceType
freshType = forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state forall a b. (a -> b) -> a -> b
$ \CheckState
st -> do
  let
    t :: Int
t = CheckState -> Int
checkNextType CheckState
st
    st' :: CheckState
st' = CheckState
st { checkNextType :: Int
checkNextType = Int
t forall a. Num a => a -> a -> a
+ Int
2
             , checkSubstitution :: Substitution
checkSubstitution =
                 (CheckState -> Substitution
checkSubstitution CheckState
st) { substUnsolved :: Map Int (UnkLevel, SourceType)
substUnsolved = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
t (NonEmpty Int -> UnkLevel
UnkLevel (forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
t), SourceType
E.kindType)
                                                        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Int
t forall a. Num a => a -> a -> a
+ Int
1) (NonEmpty Int -> UnkLevel
UnkLevel (forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
t forall a. Num a => a -> a -> a
+ Int
1)), Int -> SourceType
srcTUnknown Int
t)
                                                        forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution -> Map Int (UnkLevel, SourceType)
substUnsolved
                                                        forall a b. (a -> b) -> a -> b
$ CheckState -> Substitution
checkSubstitution CheckState
st
                                        }
             }
  (Int -> SourceType
srcTUnknown (Int
t forall a. Num a => a -> a -> a
+ Int
1), CheckState
st')

-- | Generate a fresh type variable with a known kind.
freshTypeWithKind :: (MonadState CheckState m) => SourceType -> m SourceType
freshTypeWithKind :: forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind SourceType
kind = forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state forall a b. (a -> b) -> a -> b
$ \CheckState
st -> do
  let
    t :: Int
t = CheckState -> Int
checkNextType CheckState
st
    st' :: CheckState
st' = CheckState
st { checkNextType :: Int
checkNextType = Int
t forall a. Num a => a -> a -> a
+ Int
1
             , checkSubstitution :: Substitution
checkSubstitution =
                 (CheckState -> Substitution
checkSubstitution CheckState
st) { substUnsolved :: Map Int (UnkLevel, SourceType)
substUnsolved = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
t (NonEmpty Int -> UnkLevel
UnkLevel (forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
t), SourceType
kind) (Substitution -> Map Int (UnkLevel, SourceType)
substUnsolved (CheckState -> Substitution
checkSubstitution CheckState
st)) }
             }
  (Int -> SourceType
srcTUnknown Int
t, CheckState
st')

-- | Update the substitution to solve a type constraint
solveType :: (MonadError MultipleErrors m, MonadState CheckState m) => Int -> SourceType -> m ()
solveType :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Int -> SourceType -> m ()
solveType Int
u SourceType
t = forall e (m :: * -> *) a. MonadError e m => (e -> e) -> m a -> m a
rethrow ((ErrorMessage -> ErrorMessage) -> MultipleErrors -> MultipleErrors
onErrorMessages ErrorMessage -> ErrorMessage
withoutPosition) forall a b. (a -> b) -> a -> b
$ do
  -- We strip the position so that any errors get rethrown with the position of
  -- the original unification constraint. Otherwise errors may arise from arbitrary
  -- locations. We don't otherwise have the "correct" position on hand, since it
  -- is maintained as part of the type-checker stack.
  forall (m :: * -> *).
MonadError MultipleErrors m =>
Int -> SourceType -> m ()
occursCheck Int
u SourceType
t
  SourceType
k1 <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> m SourceType
elaborateKind SourceType
t
  Substitution
subst <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Substitution
checkSubstitution
  SourceType
k2 <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a.
(MonadError MultipleErrors m, HasCallStack) =>
Text -> m a
internalCompilerError (Text
"No kind for unification variable ?" forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (forall a. Show a => a -> String
show Int
u))) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution -> SourceType -> SourceType
substituteType Substitution
subst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
u forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution -> Map Int (UnkLevel, SourceType)
substUnsolved forall a b. (a -> b) -> a -> b
$ Substitution
subst
  SourceType
t' <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
(SourceType, SourceType) -> SourceType -> m SourceType
instantiateKind (SourceType
t, SourceType
k1) SourceType
k2
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CheckState
cs -> CheckState
cs { checkSubstitution :: Substitution
checkSubstitution =
                         (CheckState -> Substitution
checkSubstitution CheckState
cs) { substType :: Map Int SourceType
substType =
                                                    forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Int
u SourceType
t' forall a b. (a -> b) -> a -> b
$ Substitution -> Map Int SourceType
substType forall a b. (a -> b) -> a -> b
$ CheckState -> Substitution
checkSubstitution CheckState
cs
                                                }
                     }

-- | Apply a substitution to a type
substituteType :: Substitution -> SourceType -> SourceType
substituteType :: Substitution -> SourceType -> SourceType
substituteType Substitution
sub = forall a. (Type a -> Type a) -> Type a -> Type a
everywhereOnTypes SourceType -> SourceType
go
  where
  go :: SourceType -> SourceType
go (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
  go SourceType
other = SourceType
other

-- | Make sure that an unknown does not occur in a type
occursCheck :: (MonadError MultipleErrors m) => Int -> SourceType -> m ()
occursCheck :: forall (m :: * -> *).
MonadError MultipleErrors m =>
Int -> SourceType -> m ()
occursCheck Int
_ TUnknown{} = forall (m :: * -> *) a. Monad m => a -> m a
return ()
occursCheck Int
u SourceType
t = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
Monad m =>
(Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereOnTypesM SourceType -> m SourceType
go SourceType
t
  where
  go :: SourceType -> m SourceType
go (TUnknown SourceAnn
_ Int
u') | Int
u forall a. Eq a => a -> a -> Bool
== Int
u' = 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
InfiniteType forall a b. (a -> b) -> a -> b
$ SourceType
t
  go SourceType
other = forall (m :: * -> *) a. Monad m => a -> m a
return SourceType
other

-- | Compute a list of all unknowns appearing in a type
unknownsInType :: Type a -> [(a, Int)]
unknownsInType :: forall a. Type a -> [(a, Int)]
unknownsInType Type a
t = forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. Type a -> [(a, Int)] -> [(a, Int)]
go Type a
t []
  where
  go :: Type a -> [(a, Int)] -> [(a, Int)]
  go :: forall a. Type a -> [(a, Int)] -> [(a, Int)]
go (TUnknown a
ann Int
u) = ((a
ann, Int
u) forall a. a -> [a] -> [a]
:)
  go Type a
_ = forall a. a -> a
id

-- | Unify two types, updating the current substitution
unifyTypes :: (MonadError MultipleErrors m, MonadState CheckState m) => SourceType -> SourceType -> m ()
unifyTypes :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
t1 SourceType
t2 = do
  Substitution
sub <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Substitution
checkSubstitution
  forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint (SourceType -> SourceType -> ErrorMessageHint
ErrorUnifyingTypes SourceType
t1 SourceType
t2) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes' (Substitution -> SourceType -> SourceType
substituteType Substitution
sub SourceType
t1) (Substitution -> SourceType -> SourceType
substituteType Substitution
sub SourceType
t2)
  where
  unifyTypes' :: SourceType -> SourceType -> m ()
unifyTypes' (TUnknown SourceAnn
_ Int
u1) (TUnknown SourceAnn
_ Int
u2) | Int
u1 forall a. Eq a => a -> a -> Bool
== Int
u2 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  unifyTypes' (TUnknown SourceAnn
_ Int
u) SourceType
t = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Int -> SourceType -> m ()
solveType Int
u SourceType
t
  unifyTypes' SourceType
t (TUnknown SourceAnn
_ Int
u) = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Int -> SourceType -> m ()
solveType Int
u SourceType
t
  unifyTypes' (ForAll SourceAnn
ann1 Text
ident1 Maybe SourceType
mbK1 SourceType
ty1 Maybe SkolemScope
sc1) (ForAll SourceAnn
ann2 Text
ident2 Maybe SourceType
mbK2 SourceType
ty2 Maybe SkolemScope
sc2) =
    case (Maybe SkolemScope
sc1, Maybe SkolemScope
sc2) of
      (Just SkolemScope
sc1', Just SkolemScope
sc2') -> do
        Int
sko <- forall (m :: * -> *). MonadState CheckState m => m Int
newSkolemConstant
        let sk1 :: SourceType
sk1 = forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize SourceAnn
ann1 Text
ident1 Maybe SourceType
mbK1 Int
sko SkolemScope
sc1' SourceType
ty1
        let sk2 :: SourceType
sk2 = forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize SourceAnn
ann2 Text
ident2 Maybe SourceType
mbK2 Int
sko SkolemScope
sc2' SourceType
ty2
        SourceType
sk1 forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
`unifyTypes` SourceType
sk2
      (Maybe SkolemScope, Maybe SkolemScope)
_ -> forall a. HasCallStack => String -> a
internalError String
"unifyTypes: unspecified skolem scope"
  unifyTypes' (ForAll SourceAnn
ann Text
ident Maybe SourceType
mbK SourceType
ty1 (Just SkolemScope
sc)) SourceType
ty2 = do
    Int
sko <- forall (m :: * -> *). MonadState CheckState m => m Int
newSkolemConstant
    let sk :: SourceType
sk = forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize SourceAnn
ann Text
ident Maybe SourceType
mbK Int
sko SkolemScope
sc SourceType
ty1
    SourceType
sk forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
`unifyTypes` SourceType
ty2
  unifyTypes' ForAll{} SourceType
_ = forall a. HasCallStack => String -> a
internalError String
"unifyTypes: unspecified skolem scope"
  unifyTypes' SourceType
ty f :: SourceType
f@ForAll{} = SourceType
f forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
`unifyTypes` SourceType
ty
  unifyTypes' (TypeVar SourceAnn
_ Text
v1) (TypeVar SourceAnn
_ Text
v2) | Text
v1 forall a. Eq a => a -> a -> Bool
== Text
v2 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  unifyTypes' ty1 :: SourceType
ty1@(TypeConstructor SourceAnn
_ Qualified (ProperName 'TypeName)
c1) ty2 :: SourceType
ty2@(TypeConstructor SourceAnn
_ Qualified (ProperName 'TypeName)
c2) =
    forall e (m :: * -> *). MonadError e m => e -> Bool -> m ()
guardWith (SimpleErrorMessage -> MultipleErrors
errorMessage (SourceType -> SourceType -> SimpleErrorMessage
TypesDoNotUnify SourceType
ty1 SourceType
ty2)) (Qualified (ProperName 'TypeName)
c1 forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
c2)
  unifyTypes' (TypeLevelString SourceAnn
_ PSString
s1) (TypeLevelString SourceAnn
_ PSString
s2) | PSString
s1 forall a. Eq a => a -> a -> Bool
== PSString
s2 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  unifyTypes' (TypeLevelInt    SourceAnn
_ Integer
n1) (TypeLevelInt    SourceAnn
_ Integer
n2) | Integer
n1 forall a. Eq a => a -> a -> Bool
== Integer
n2 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  unifyTypes' (TypeApp SourceAnn
_ SourceType
t3 SourceType
t4) (TypeApp SourceAnn
_ SourceType
t5 SourceType
t6) = do
    SourceType
t3 forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
`unifyTypes` SourceType
t5
    SourceType
t4 forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
`unifyTypes` SourceType
t6
  unifyTypes' (KindApp SourceAnn
_ SourceType
t3 SourceType
t4) (KindApp SourceAnn
_ SourceType
t5 SourceType
t6) = do
    SourceType
t3 forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> SourceType -> m ()
`unifyKinds'` SourceType
t5
    SourceType
t4 forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
`unifyTypes` SourceType
t6
  unifyTypes' (Skolem SourceAnn
_ Text
_ Maybe SourceType
_ Int
s1 SkolemScope
_) (Skolem SourceAnn
_ Text
_ Maybe SourceType
_ Int
s2 SkolemScope
_) | Int
s1 forall a. Eq a => a -> a -> Bool
== Int
s2 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  unifyTypes' (KindedType SourceAnn
_ SourceType
ty1 SourceType
_) SourceType
ty2 = SourceType
ty1 forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
`unifyTypes` SourceType
ty2
  unifyTypes' SourceType
ty1 (KindedType SourceAnn
_ SourceType
ty2 SourceType
_) = SourceType
ty1 forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
`unifyTypes` SourceType
ty2
  unifyTypes' r1 :: SourceType
r1@RCons{} SourceType
r2 = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2
  unifyTypes' SourceType
r1 r2 :: SourceType
r2@RCons{} = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2
  unifyTypes' r1 :: SourceType
r1@REmptyKinded{} SourceType
r2 = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2
  unifyTypes' SourceType
r1 r2 :: SourceType
r2@REmptyKinded{} = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2
  unifyTypes' (ConstrainedType SourceAnn
_ Constraint SourceAnn
c1 SourceType
ty1) (ConstrainedType SourceAnn
_ Constraint SourceAnn
c2 SourceType
ty2)
    | forall a. Constraint a -> Qualified (ProperName 'ClassName)
constraintClass Constraint SourceAnn
c1 forall a. Eq a => a -> a -> Bool
== forall a. Constraint a -> Qualified (ProperName 'ClassName)
constraintClass Constraint SourceAnn
c2 Bool -> Bool -> Bool
&& forall a. Constraint a -> Maybe ConstraintData
constraintData Constraint SourceAnn
c1 forall a. Eq a => a -> a -> Bool
== forall a. Constraint a -> Maybe ConstraintData
constraintData Constraint SourceAnn
c2 = do
        forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes) (forall a. Constraint a -> [Type a]
constraintArgs Constraint SourceAnn
c1 forall a b. [a] -> [b] -> [(a, b)]
`zip` forall a. Constraint a -> [Type a]
constraintArgs Constraint SourceAnn
c2)
        SourceType
ty1 forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
`unifyTypes` SourceType
ty2
  unifyTypes' ty1 :: SourceType
ty1@ConstrainedType{} SourceType
ty2 =
    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
ConstrainedTypeUnified SourceType
ty1 SourceType
ty2
  unifyTypes' SourceType
t3 t4 :: SourceType
t4@ConstrainedType{} = SourceType -> SourceType -> m ()
unifyTypes' SourceType
t4 SourceType
t3
  unifyTypes' SourceType
t3 SourceType
t4 =
    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
TypesDoNotUnify SourceType
t3 SourceType
t4

-- | Unify two rows, updating the current substitution
--
-- Common labels are identified and unified. Remaining labels and types are unified with a
-- trailing row unification variable, if appropriate.
unifyRows :: forall m. (MonadError MultipleErrors m, MonadState CheckState m) => SourceType -> SourceType -> m ()
unifyRows :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyRows SourceType
r1 SourceType
r2 = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
matches forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ([RowListItem SourceAnn], SourceType)
-> ([RowListItem SourceAnn], SourceType) -> m ()
unifyTails (([RowListItem SourceAnn], SourceType),
 ([RowListItem SourceAnn], SourceType))
rest where
  unifyTypesWithLabel :: Label -> SourceType -> SourceType -> m ()
unifyTypesWithLabel 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
$ forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
t1 SourceType
t2

  ([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 forall {m :: * -> *}.
(MonadState CheckState m, MonadError MultipleErrors m) =>
Label -> SourceType -> SourceType -> m ()
unifyTypesWithLabel SourceType
r1 SourceType
r2

  unifyTails :: ([RowListItem SourceAnn], SourceType) -> ([RowListItem SourceAnn], SourceType) -> m ()
  unifyTails :: ([RowListItem SourceAnn], SourceType)
-> ([RowListItem SourceAnn], SourceType) -> m ()
unifyTails ([], TUnknown SourceAnn
_ Int
u)    ([RowListItem SourceAnn]
sd, SourceType
r)               = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Int -> SourceType -> m ()
solveType Int
u (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
sd, SourceType
r))
  unifyTails ([RowListItem SourceAnn]
sd, SourceType
r)               ([], TUnknown SourceAnn
_ Int
u)    = forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Int -> SourceType -> m ()
solveType Int
u (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
sd, SourceType
r))
  unifyTails ([], REmptyKinded SourceAnn
_ Maybe SourceType
_) ([], REmptyKinded SourceAnn
_ Maybe SourceType
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  unifyTails ([], TypeVar SourceAnn
_ Text
v1)    ([], TypeVar SourceAnn
_ Text
v2)    | Text
v1 forall a. Eq a => a -> a -> Bool
== Text
v2 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  unifyTails ([], Skolem SourceAnn
_ Text
_ Maybe SourceType
_ Int
s1 SkolemScope
_) ([], Skolem SourceAnn
_ Text
_ Maybe SourceType
_ Int
s2 SkolemScope
_) | Int
s1 forall a. Eq a => a -> a -> Bool
== Int
s2 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  unifyTails ([RowListItem SourceAnn]
sd1, TUnknown SourceAnn
a Int
u1)  ([RowListItem SourceAnn]
sd2, TUnknown SourceAnn
_ Int
u2)  | Int
u1 forall a. Eq a => a -> a -> Bool
/= Int
u2 = do
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [RowListItem SourceAnn]
sd1 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadError MultipleErrors m =>
Int -> SourceType -> m ()
occursCheck Int
u2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. RowListItem a -> Type a
rowListType
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [RowListItem SourceAnn]
sd2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadError MultipleErrors m =>
Int -> SourceType -> m ()
occursCheck Int
u1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. RowListItem a -> Type a
rowListType
    SourceType
rest' <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind 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
elaborateKind (forall a. a -> Int -> Type a
TUnknown SourceAnn
a Int
u1)
    forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Int -> SourceType -> m ()
solveType Int
u1 (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
sd2, SourceType
rest'))
    forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Int -> SourceType -> m ()
solveType Int
u2 (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
sd1, SourceType
rest'))
  unifyTails ([RowListItem SourceAnn], SourceType)
_ ([RowListItem SourceAnn], 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
TypesDoNotUnify SourceType
r1 SourceType
r2

-- |
-- Replace type wildcards with unknowns
--
replaceTypeWildcards :: (MonadWriter MultipleErrors m, MonadState CheckState m) => SourceType -> m SourceType
replaceTypeWildcards :: forall (m :: * -> *).
(MonadWriter MultipleErrors m, MonadState CheckState m) =>
SourceType -> m SourceType
replaceTypeWildcards = forall (m :: * -> *) a.
Monad m =>
(Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereOnTypesM forall {m :: * -> *}.
(MonadState CheckState m, MonadWriter MultipleErrors m) =>
SourceType -> m SourceType
replace
  where
  replace :: SourceType -> m SourceType
replace (TypeWildcard SourceAnn
ann WildcardData
wdata) = do
    SourceType
t <- forall (m :: * -> *). MonadState CheckState m => m SourceType
freshType
    Context
ctx <- forall (m :: * -> *). MonadState CheckState m => m Context
getLocalContext
    let err :: Maybe SimpleErrorMessage
err = case WildcardData
wdata of
          HoleWildcard Text
n -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Text
-> SourceType -> Context -> Maybe TypeSearch -> SimpleErrorMessage
HoleInferredType Text
n SourceType
t Context
ctx forall a. Maybe a
Nothing
          WildcardData
UnnamedWildcard -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ SourceType -> Context -> SimpleErrorMessage
WildcardInferredType SourceType
t Context
ctx
          WildcardData
IgnoredWildcard -> forall a. Maybe a
Nothing
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Maybe SimpleErrorMessage
err forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadWriter MultipleErrors m =>
SourceSpan -> m a -> m a
warnWithPosition (forall a b. (a, b) -> a
fst SourceAnn
ann) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage
    forall (m :: * -> *) a. Monad m => a -> m a
return SourceType
t
  replace SourceType
other = forall (m :: * -> *) a. Monad m => a -> m a
return SourceType
other

-- |
-- Replace outermost unsolved unification variables with named type variables
--
varIfUnknown :: forall m. (MonadState CheckState m) => [(Unknown, SourceType)] -> SourceType -> m SourceType
varIfUnknown :: forall (m :: * -> *).
MonadState CheckState m =>
[(Int, SourceType)] -> SourceType -> m SourceType
varIfUnknown [(Int, SourceType)]
unks SourceType
ty = do
  [(SourceAnn, (Text, Maybe SourceType))]
bn' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Int, SourceType) -> m (SourceAnn, (Text, Maybe SourceType))
toBinding [(Int, SourceType)]
unks
  SourceType
ty' <- SourceType -> m SourceType
go SourceType
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 -> Type a
mkForAll [(SourceAnn, (Text, Maybe SourceType))]
bn' SourceType
ty'
  where
  toName :: Unknown -> m T.Text
  toName :: Int -> m Text
toName Int
u = (forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (forall a. Show a => a -> String
show Int
u)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe Text
"t" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
Int -> m (Maybe Text)
lookupUnkName Int
u

  toBinding :: (Unknown, SourceType) -> m (SourceAnn, (T.Text, Maybe SourceType))
  toBinding :: (Int, SourceType) -> m (SourceAnn, (Text, Maybe SourceType))
toBinding (Int
u, SourceType
k) = do
    Text
u' <- Int -> m Text
toName Int
u
    SourceType
k' <- SourceType -> m SourceType
go SourceType
k
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Type a -> a
getAnnForType SourceType
ty, (Text
u', forall a. a -> Maybe a
Just SourceType
k'))

  go :: SourceType -> m SourceType
  go :: SourceType -> m SourceType
go = forall (m :: * -> *) a.
Monad m =>
(Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereOnTypesM forall a b. (a -> b) -> a -> b
$ \case
    (TUnknown SourceAnn
ann Int
u) ->
      forall a. a -> Text -> Type a
TypeVar SourceAnn
ann forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m Text
toName Int
u
    SourceType
t -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
t