-- |
-- 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
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 qualified Data.Map as M
import qualified Data.Text as T

import Language.PureScript.Crash
import qualified Language.PureScript.Environment as E
import Language.PureScript.Errors
import Language.PureScript.TypeChecker.Kinds (elaborateKind, instantiateKind, unifyKinds')
import Language.PureScript.TypeChecker.Monad
import Language.PureScript.TypeChecker.Skolems
import Language.PureScript.Types

-- | 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
  ([m ()]
matches, (([RowListItem SourceAnn], SourceType),
 ([RowListItem SourceAnn], SourceType))
rest) = forall a r.
(Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes 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