module Language.Futhark.TypeChecker.TySolve
  ( Type,
    Solution,
    UnconTyVar,
    solve,
  )
where

import Control.Monad
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.ST
import Data.Bifunctor
import Data.List qualified as L
import Data.Loc
import Data.Map qualified as M
import Data.Maybe
import Data.Set qualified as S
import Futhark.Util.Pretty
import Language.Futhark
import Language.Futhark.TypeChecker.Constraints
import Language.Futhark.TypeChecker.Error
import Language.Futhark.TypeChecker.Monad (Notes, TypeError (..), aNote, withIndexLink)
import Language.Futhark.TypeChecker.UnionFind

-- | The type representation used by the constraint solver. Agnostic
-- to sizes and freshness.
type Type = CtType ()

type UF s = M.Map TyVar (TyVarNode s)

newtype SolverState s = SolverState {forall s. SolverState s -> UF s
solverTyVars :: UF s}

newtype SolveM s a = SolveM
  { forall s a.
SolveM s a -> ExceptT TypeError (ReaderT (SolverState s) (ST s)) a
runSolveM :: ExceptT TypeError (ReaderT (SolverState s) (ST s)) a
  }
  deriving ((forall a b. (a -> b) -> SolveM s a -> SolveM s b)
-> (forall a b. a -> SolveM s b -> SolveM s a)
-> Functor (SolveM s)
forall a b. a -> SolveM s b -> SolveM s a
forall a b. (a -> b) -> SolveM s a -> SolveM s b
forall s a b. a -> SolveM s b -> SolveM s a
forall s a b. (a -> b) -> SolveM s a -> SolveM s b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall s a b. (a -> b) -> SolveM s a -> SolveM s b
fmap :: forall a b. (a -> b) -> SolveM s a -> SolveM s b
$c<$ :: forall s a b. a -> SolveM s b -> SolveM s a
<$ :: forall a b. a -> SolveM s b -> SolveM s a
Functor, Functor (SolveM s)
Functor (SolveM s) =>
(forall a. a -> SolveM s a)
-> (forall a b. SolveM s (a -> b) -> SolveM s a -> SolveM s b)
-> (forall a b c.
    (a -> b -> c) -> SolveM s a -> SolveM s b -> SolveM s c)
-> (forall a b. SolveM s a -> SolveM s b -> SolveM s b)
-> (forall a b. SolveM s a -> SolveM s b -> SolveM s a)
-> Applicative (SolveM s)
forall s. Functor (SolveM s)
forall a. a -> SolveM s a
forall s a. a -> SolveM s a
forall a b. SolveM s a -> SolveM s b -> SolveM s a
forall a b. SolveM s a -> SolveM s b -> SolveM s b
forall a b. SolveM s (a -> b) -> SolveM s a -> SolveM s b
forall s a b. SolveM s a -> SolveM s b -> SolveM s a
forall s a b. SolveM s a -> SolveM s b -> SolveM s b
forall s a b. SolveM s (a -> b) -> SolveM s a -> SolveM s b
forall a b c.
(a -> b -> c) -> SolveM s a -> SolveM s b -> SolveM s c
forall s a b c.
(a -> b -> c) -> SolveM s a -> SolveM s b -> SolveM s c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall s a. a -> SolveM s a
pure :: forall a. a -> SolveM s a
$c<*> :: forall s a b. SolveM s (a -> b) -> SolveM s a -> SolveM s b
<*> :: forall a b. SolveM s (a -> b) -> SolveM s a -> SolveM s b
$cliftA2 :: forall s a b c.
(a -> b -> c) -> SolveM s a -> SolveM s b -> SolveM s c
liftA2 :: forall a b c.
(a -> b -> c) -> SolveM s a -> SolveM s b -> SolveM s c
$c*> :: forall s a b. SolveM s a -> SolveM s b -> SolveM s b
*> :: forall a b. SolveM s a -> SolveM s b -> SolveM s b
$c<* :: forall s a b. SolveM s a -> SolveM s b -> SolveM s a
<* :: forall a b. SolveM s a -> SolveM s b -> SolveM s a
Applicative, Applicative (SolveM s)
Applicative (SolveM s) =>
(forall a b. SolveM s a -> (a -> SolveM s b) -> SolveM s b)
-> (forall a b. SolveM s a -> SolveM s b -> SolveM s b)
-> (forall a. a -> SolveM s a)
-> Monad (SolveM s)
forall s. Applicative (SolveM s)
forall a. a -> SolveM s a
forall s a. a -> SolveM s a
forall a b. SolveM s a -> SolveM s b -> SolveM s b
forall a b. SolveM s a -> (a -> SolveM s b) -> SolveM s b
forall s a b. SolveM s a -> SolveM s b -> SolveM s b
forall s a b. SolveM s a -> (a -> SolveM s b) -> SolveM s b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall s a b. SolveM s a -> (a -> SolveM s b) -> SolveM s b
>>= :: forall a b. SolveM s a -> (a -> SolveM s b) -> SolveM s b
$c>> :: forall s a b. SolveM s a -> SolveM s b -> SolveM s b
>> :: forall a b. SolveM s a -> SolveM s b -> SolveM s b
$creturn :: forall s a. a -> SolveM s a
return :: forall a. a -> SolveM s a
Monad, MonadError TypeError, MonadReader (SolverState s))

-- | A solution maps a type variable to its substitution. This
-- substitution is complete, in the sense there are no right-hand
-- sides that contain a type variable.
type Solution = M.Map TyVar (Either [PrimType] (TypeBase () NoMode))

-- | An unconstrained type variable comprises a name and (ironically)
-- a constraint on how it can be instantiated.
type UnconTyVar = (VName, Liftedness)

liftST :: ST s a -> SolveM s a
liftST :: forall s a. ST s a -> SolveM s a
liftST = ExceptT TypeError (ReaderT (SolverState s) (ST s)) a -> SolveM s a
forall s a.
ExceptT TypeError (ReaderT (SolverState s) (ST s)) a -> SolveM s a
SolveM (ExceptT TypeError (ReaderT (SolverState s) (ST s)) a
 -> SolveM s a)
-> (ST s a -> ExceptT TypeError (ReaderT (SolverState s) (ST s)) a)
-> ST s a
-> SolveM s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReaderT (SolverState s) (ST s) a
-> ExceptT TypeError (ReaderT (SolverState s) (ST s)) a
forall (m :: * -> *) a. Monad m => m a -> ExceptT TypeError m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ReaderT (SolverState s) (ST s) a
 -> ExceptT TypeError (ReaderT (SolverState s) (ST s)) a)
-> (ST s a -> ReaderT (SolverState s) (ST s) a)
-> ST s a
-> ExceptT TypeError (ReaderT (SolverState s) (ST s)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ST s a -> ReaderT (SolverState s) (ST s) a
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT (SolverState s) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

getSol' :: TyVarNode s -> SolveM s TyVarSol
getSol' :: forall s. TyVarNode s -> SolveM s TyVarSol
getSol' = ST s TyVarSol -> SolveM s TyVarSol
forall s a. ST s a -> SolveM s a
liftST (ST s TyVarSol -> SolveM s TyVarSol)
-> (TyVarNode s -> ST s TyVarSol)
-> TyVarNode s
-> SolveM s TyVarSol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarNode s -> ST s TyVarSol
forall s. TyVarNode s -> ST s TyVarSol
getSol

union' :: TyVarNode s -> TyVarNode s -> SolveM s ()
union' :: forall s. TyVarNode s -> TyVarNode s -> SolveM s ()
union' TyVarNode s
tv1 TyVarNode s
tv2 = ST s () -> SolveM s ()
forall s a. ST s a -> SolveM s a
liftST (ST s () -> SolveM s ()) -> ST s () -> SolveM s ()
forall a b. (a -> b) -> a -> b
$ TyVarNode s -> TyVarNode s -> ST s ()
forall s. TyVarNode s -> TyVarNode s -> ST s ()
union TyVarNode s
tv1 TyVarNode s
tv2

unionNewSol' :: forall s. TyVarNode s -> TyVarNode s -> TyVarSol -> SolveM s ()
unionNewSol' TyVarNode s
tv1 TyVarNode s
tv2 TyVarSol
new_sol = ST s () -> SolveM s ()
forall s a. ST s a -> SolveM s a
liftST (ST s () -> SolveM s ()) -> ST s () -> SolveM s ()
forall a b. (a -> b) -> a -> b
$ TyVarNode s -> TyVarNode s -> TyVarSol -> ST s ()
forall s. TyVarNode s -> TyVarNode s -> TyVarSol -> ST s ()
unionNewSol TyVarNode s
tv1 TyVarNode s
tv2 TyVarSol
new_sol

unionNewSol' :: TyVarNode s -> TyVarNode s -> TyVarSol -> SolveM s ()
getKey' :: TyVarNode s -> SolveM s TyVar
getKey' :: forall s. TyVarNode s -> SolveM s TyVar
getKey' = ST s TyVar -> SolveM s TyVar
forall s a. ST s a -> SolveM s a
liftST (ST s TyVar -> SolveM s TyVar)
-> (TyVarNode s -> ST s TyVar) -> TyVarNode s -> SolveM s TyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarNode s -> ST s TyVar
forall s. TyVarNode s -> ST s TyVar
getKey

initializeState :: TyParams -> TyVars () -> ST s (SolverState s)
initializeState :: forall s. TyParams -> TyVars () -> ST s (SolverState s)
initializeState TyParams
typarams TyVars ()
tyvars = do
  tyvars' <- (TyVar -> (Level, TyVarInfo ()) -> ST s (TyVarNode s))
-> TyVars () -> ST s (UF s)
forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
M.traverseWithKey TyVar -> (Level, TyVarInfo ()) -> ST s (TyVarNode s)
forall {a} {s}. TyVar -> (a, TyVarInfo ()) -> ST s (TyVarNode s)
f TyVars ()
tyvars
  typarams' <- M.traverseWithKey g typarams
  pure $ SolverState $ typarams' <> tyvars'
  where
    f :: TyVar -> (a, TyVarInfo ()) -> ST s (TyVarNode s)
f TyVar
tv (a
_lvl, TyVarInfo ()
info) = TyVar -> TyVarInfo () -> ST s (TyVarNode s)
forall s. TyVar -> TyVarInfo () -> ST s (TyVarNode s)
makeTyVarNode TyVar
tv TyVarInfo ()
info
    g :: TyVar -> (Level, Liftedness, Loc) -> ST s (TyVarNode s)
g TyVar
tv (Level
lvl, Liftedness
lft, Loc
loc) = TyVar -> Level -> Liftedness -> Loc -> ST s (TyVarNode s)
forall s. TyVar -> Level -> Liftedness -> Loc -> ST s (TyVarNode s)
makeTyParamNode TyVar
tv Level
lvl Liftedness
lft Loc
loc

typeError :: Loc -> Notes -> Doc () -> SolveM s ()
typeError :: forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError Loc
loc Notes
notes Doc ()
msg =
  TypeError -> SolveM s ()
forall a. TypeError -> SolveM s a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> SolveM s ()) -> TypeError -> SolveM s ()
forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc Notes
notes Doc ()
msg

typeVar :: (Monoid o) => VName -> TypeBase dim o
typeVar :: forall o dim. Monoid o => TyVar -> TypeBase dim o
typeVar TyVar
v = ScalarTypeBase dim o -> TypeBase dim o
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase dim o -> TypeBase dim o)
-> ScalarTypeBase dim o -> TypeBase dim o
forall a b. (a -> b) -> a -> b
$ o -> QualName TyVar -> [TypeArg dim] -> ScalarTypeBase dim o
forall dim o.
o -> QualName TyVar -> [TypeArg dim] -> ScalarTypeBase dim o
TypeVar o
forall a. Monoid a => a
mempty (TyVar -> QualName TyVar
forall v. v -> QualName v
qualName TyVar
v) []

cannotUnify ::
  Reason Type ->
  Notes ->
  BreadCrumbs ->
  Type ->
  Type ->
  SolveM s ()
cannotUnify :: forall s.
Reason Type -> Notes -> BreadCrumbs -> Type -> Type -> SolveM s ()
cannotUnify Reason Type
reason Notes
notes BreadCrumbs
bcs Type
t1 Type
t2 = do
  t1' <- Type -> SolveM s Type
forall o s. Monoid o => TypeBase () o -> SolveM s (TypeBase () o)
substTyVars Type
t1
  t2' <- substTyVars t2
  case reason of
    Reason Loc
loc ->
      Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError Loc
loc Notes
notes (Doc () -> SolveM s ())
-> ([Doc ()] -> Doc ()) -> [Doc ()] -> SolveM s ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
stack ([Doc ()] -> SolveM s ()) -> [Doc ()] -> SolveM s ()
forall a b. (a -> b) -> a -> b
$
        [ Doc ()
"Cannot unify",
          Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty Type
t1'),
          Doc ()
"with",
          Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty Type
t2')
        ]
          [Doc ()] -> [Doc ()] -> [Doc ()]
forall a. Semigroup a => a -> a -> a
<> [BreadCrumbs -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. BreadCrumbs -> Doc ann
pretty BreadCrumbs
bcs | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ BreadCrumbs -> Bool
hasNoBreadCrumbs BreadCrumbs
bcs]
    ReasonPatMatch Loc
loc PatBase NoInfo TyVar StructType
pat Type
value_t ->
      Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError Loc
loc Notes
notes (Doc () -> SolveM s ())
-> ([Doc ()] -> Doc ()) -> [Doc ()] -> SolveM s ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
stack ([Doc ()] -> SolveM s ()) -> [Doc ()] -> SolveM s ()
forall a b. (a -> b) -> a -> b
$
        [ Doc ()
"Pattern",
          Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
align (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ PatBase NoInfo TyVar StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. PatBase NoInfo TyVar StructType -> Doc ann
pretty PatBase NoInfo TyVar StructType
pat,
          Doc ()
"cannot match value of type",
          Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
align (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty Type
value_t
        ]
          [Doc ()] -> [Doc ()] -> [Doc ()]
forall a. Semigroup a => a -> a -> a
<> [BreadCrumbs -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. BreadCrumbs -> Doc ann
pretty BreadCrumbs
bcs | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ BreadCrumbs -> Bool
hasNoBreadCrumbs BreadCrumbs
bcs]
    ReasonAscription Loc
loc Type
expected Type
actual ->
      Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError Loc
loc Notes
notes (Doc () -> SolveM s ())
-> ([Doc ()] -> Doc ()) -> [Doc ()] -> SolveM s ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
stack ([Doc ()] -> SolveM s ()) -> [Doc ()] -> SolveM s ()
forall a b. (a -> b) -> a -> b
$
        [ Doc ()
"Expression does not have expected type from type ascription.",
          Doc ()
"Expected:" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
align (Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty Type
expected),
          Doc ()
"Actual:  " Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
align (Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty Type
actual)
        ]
          [Doc ()] -> [Doc ()] -> [Doc ()]
forall a. Semigroup a => a -> a -> a
<> [BreadCrumbs -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. BreadCrumbs -> Doc ann
pretty BreadCrumbs
bcs | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ BreadCrumbs -> Bool
hasNoBreadCrumbs BreadCrumbs
bcs]
    ReasonRetType Loc
loc Type
expected Type
actual -> do
      expected' <- Type -> SolveM s Type
forall o s. Monoid o => TypeBase () o -> SolveM s (TypeBase () o)
substTyVars Type
expected
      actual' <- substTyVars actual
      typeError loc notes . stack $
        [ "Function body does not have expected type.",
          "Expected:" <+> align (pretty expected'),
          "Actual:  " <+> align (pretty actual')
        ]
          <> [pretty bcs | not $ hasNoBreadCrumbs bcs]
    ReasonApply Loc
loc (Maybe (QualName TyVar), Level)
f Exp
e Type
expected Type
actual -> do
      expected' <- Type -> SolveM s Type
forall o s. Monoid o => TypeBase () o -> SolveM s (TypeBase () o)
substTyVars Type
expected
      actual' <- substTyVars actual
      typeError loc notes . stack $
        [ header,
          "Expected:" <+> align (pretty expected'),
          "Actual:  " <+> align (pretty actual')
        ]
      where
        header :: Doc ann
header =
          case (Maybe (QualName TyVar), Level)
f of
            (Maybe (QualName TyVar)
Nothing, Level
_) ->
              Doc ann
"Cannot apply function to"
                Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Doc (ZonkAny 0) -> Doc ann
forall a b. Doc a -> Doc b
shorten (Doc (ZonkAny 0) -> Doc ann) -> Doc (ZonkAny 0) -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc (ZonkAny 0) -> Doc (ZonkAny 0)
forall ann. Doc ann -> Doc ann
group (Doc (ZonkAny 0) -> Doc (ZonkAny 0))
-> Doc (ZonkAny 0) -> Doc (ZonkAny 0)
forall a b. (a -> b) -> a -> b
$ Exp -> Doc (ZonkAny 0)
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
e)
                Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" (invalid type)."
            (Just QualName TyVar
fname, Level
_) ->
              Doc ann
"Cannot apply"
                Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (QualName TyVar -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName TyVar -> Doc ann
pretty QualName TyVar
fname)
                Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"to"
                Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc (ZonkAny 1) -> Doc ann
forall a b. Doc a -> Doc b
shorten (Doc (ZonkAny 1) -> Doc ann) -> Doc (ZonkAny 1) -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc (ZonkAny 1) -> Doc (ZonkAny 1)
forall ann. Doc ann -> Doc ann
group (Doc (ZonkAny 1) -> Doc (ZonkAny 1))
-> Doc (ZonkAny 1) -> Doc (ZonkAny 1)
forall a b. (a -> b) -> a -> b
$ Exp -> Doc (ZonkAny 1)
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
e)
                Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" (invalid type)."
    ReasonApplySplit Loc
loc (Maybe (QualName TyVar)
fname, Level
0) Exp
_ Type
ftype ->
      Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError Loc
loc Notes
notes (Doc () -> SolveM s ()) -> Doc () -> SolveM s ()
forall a b. (a -> b) -> a -> b
$
        [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
stack
          [ Doc ()
"Cannot apply"
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
forall {ann}. Doc ann
fname'
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"as function, as it has non-function type:"
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
align (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty Type
ftype)
          ]
      where
        fname' :: Doc ann
fname' = Doc ann
-> (QualName TyVar -> Doc ann) -> Maybe (QualName TyVar) -> Doc ann
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
"expression" (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Doc ann -> Doc ann)
-> (QualName TyVar -> Doc ann) -> QualName TyVar -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName TyVar -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName TyVar -> Doc ann
pretty) Maybe (QualName TyVar)
fname
    ReasonApplySplit Loc
loc (Maybe (QualName TyVar)
fname, Level
i) Exp
e Type
_ ->
      Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError Loc
loc Notes
notes (Doc () -> SolveM s ()) -> Doc () -> SolveM s ()
forall a b. (a -> b) -> a -> b
$
        [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
stack
          [ Doc ()
"Cannot apply"
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
forall {ann}. Doc ann
fname'
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"to"
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
align (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ Doc (ZonkAny 2) -> Doc ()
forall a b. Doc a -> Doc b
shorten (Doc (ZonkAny 2) -> Doc ()) -> Doc (ZonkAny 2) -> Doc ()
forall a b. (a -> b) -> a -> b
$ Doc (ZonkAny 2) -> Doc (ZonkAny 2)
forall ann. Doc ann -> Doc ann
group (Doc (ZonkAny 2) -> Doc (ZonkAny 2))
-> Doc (ZonkAny 2) -> Doc (ZonkAny 2)
forall a b. (a -> b) -> a -> b
$ Exp -> Doc (ZonkAny 2)
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
e)
              Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
".",
            Doc ()
"Function accepts only" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Level -> Doc ()
forall ann. Level -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Level
i Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"arguments."
          ]
      where
        fname' :: Doc ann
fname' = Doc ann
-> (QualName TyVar -> Doc ann) -> Maybe (QualName TyVar) -> Doc ann
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
"expression" (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Doc ann -> Doc ann)
-> (QualName TyVar -> Doc ann) -> QualName TyVar -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName TyVar -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName TyVar -> Doc ann
pretty) Maybe (QualName TyVar)
fname
    ReasonBranches Loc
loc Type
former Type
latter -> do
      former' <- Type -> SolveM s Type
forall o s. Monoid o => TypeBase () o -> SolveM s (TypeBase () o)
substTyVars Type
former
      latter' <- substTyVars latter
      typeError loc notes . stack $
        [ "Branches differ in type.",
          "Former:" <+> pretty former',
          "Latter:" <+> pretty latter'
        ]

unsharedConstructorsMsg :: M.Map Name t -> M.Map Name t -> Doc a
unsharedConstructorsMsg :: forall t a. Map Name t -> Map Name t -> Doc a
unsharedConstructorsMsg Map Name t
cs1 Map Name t
cs2 =
  Doc a
"Unshared constructors:" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc a] -> Doc a
forall a. [Doc a] -> Doc a
commasep ((Name -> Doc a) -> [Name] -> [Doc a]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc a
"#" Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<>) (Doc a -> Doc a) -> (Name -> Doc a) -> Name -> Doc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty) [Name]
missing) Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<> Doc a
"."
  where
    missing :: [Name]
missing =
      (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Map Name t -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name t
cs1) (Map Name t -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name t
cs2)
        [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Map Name t -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name t
cs2) (Map Name t -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name t
cs1)

substTyVars :: (Monoid o) => TypeBase () o -> SolveM s (TypeBase () o)
substTyVars :: forall o s. Monoid o => TypeBase () o -> SolveM s (TypeBase () o)
substTyVars (Scalar (TypeVar o
o QualName TyVar
qn [TypeArg ()]
args)) = do
  mb_node <- TyVar -> SolveM s (Maybe (TyVarNode s))
forall s. TyVar -> SolveM s (Maybe (TyVarNode s))
maybeLookupUF (TyVar -> SolveM s (Maybe (TyVarNode s)))
-> TyVar -> SolveM s (Maybe (TyVarNode s))
forall a b. (a -> b) -> a -> b
$ QualName TyVar -> TyVar
forall vn. QualName vn -> vn
qualLeaf QualName TyVar
qn
  case mb_node of
    Just TyVarNode s
node -> do
      sol <- TyVarNode s -> SolveM s TyVarSol
forall s. TyVarNode s -> SolveM s TyVarSol
getSol' TyVarNode s
node
      qn_k <- qualName <$> getKey' node
      case sol of
        Solved Type
t -> do
          t' <- Type -> SolveM s Type
forall o s. Monoid o => TypeBase () o -> SolveM s (TypeBase () o)
substTyVars Type
t
          pure $ second (const mempty) t'
        TyVarSol
_ -> QualName TyVar -> SolveM s (TypeBase () o)
forall {s}. QualName TyVar -> SolveM s (TypeBase () o)
makeTyVar QualName TyVar
qn_k
    Maybe (TyVarNode s)
_ -> QualName TyVar -> SolveM s (TypeBase () o)
forall {s}. QualName TyVar -> SolveM s (TypeBase () o)
makeTyVar QualName TyVar
qn
  where
    makeTyVar :: QualName TyVar -> SolveM s (TypeBase () o)
makeTyVar QualName TyVar
qn' = do
      args' <- (TypeArg () -> SolveM s (TypeArg ()))
-> [TypeArg ()] -> SolveM s [TypeArg ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TypeArg () -> SolveM s (TypeArg ())
forall {s}. TypeArg () -> SolveM s (TypeArg ())
onArg [TypeArg ()]
args
      pure $ Scalar $ TypeVar o qn' args'
    onArg :: TypeArg () -> SolveM s (TypeArg ())
onArg (TypeArgType Type
t) = Type -> TypeArg ()
forall dim. TypeBase dim NoMode -> TypeArg dim
TypeArgType (Type -> TypeArg ()) -> SolveM s Type -> SolveM s (TypeArg ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> SolveM s Type
forall o s. Monoid o => TypeBase () o -> SolveM s (TypeBase () o)
substTyVars Type
t
    onArg d :: TypeArg ()
d@(TypeArgDim ()
_) = TypeArg () -> SolveM s (TypeArg ())
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeArg ()
d
substTyVars p :: TypeBase () o
p@(Scalar (Prim PrimType
_)) = TypeBase () o -> SolveM s (TypeBase () o)
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeBase () o
p
substTyVars (Scalar (Record Map Name (TypeBase () o)
fs)) =
  ScalarTypeBase () o -> TypeBase () o
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase () o -> TypeBase () o)
-> (Map Name (TypeBase () o) -> ScalarTypeBase () o)
-> Map Name (TypeBase () o)
-> TypeBase () o
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name (TypeBase () o) -> ScalarTypeBase () o
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record (Map Name (TypeBase () o) -> TypeBase () o)
-> SolveM s (Map Name (TypeBase () o)) -> SolveM s (TypeBase () o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TypeBase () o -> SolveM s (TypeBase () o))
-> Map Name (TypeBase () o) -> SolveM s (Map Name (TypeBase () o))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Name a -> f (Map Name b)
traverse TypeBase () o -> SolveM s (TypeBase () o)
forall o s. Monoid o => TypeBase () o -> SolveM s (TypeBase () o)
substTyVars Map Name (TypeBase () o)
fs
substTyVars (Scalar (Sum Map Name [TypeBase () o]
cs)) =
  ScalarTypeBase () o -> TypeBase () o
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase () o -> TypeBase () o)
-> (Map Name [TypeBase () o] -> ScalarTypeBase () o)
-> Map Name [TypeBase () o]
-> TypeBase () o
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name [TypeBase () o] -> ScalarTypeBase () o
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum (Map Name [TypeBase () o] -> TypeBase () o)
-> SolveM s (Map Name [TypeBase () o]) -> SolveM s (TypeBase () o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([TypeBase () o] -> SolveM s [TypeBase () o])
-> Map Name [TypeBase () o] -> SolveM s (Map Name [TypeBase () o])
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Name a -> f (Map Name b)
traverse ((TypeBase () o -> SolveM s (TypeBase () o))
-> [TypeBase () o] -> SolveM s [TypeBase () o]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TypeBase () o -> SolveM s (TypeBase () o)
forall o s. Monoid o => TypeBase () o -> SolveM s (TypeBase () o)
substTyVars) Map Name [TypeBase () o]
cs
substTyVars (Scalar (Arrow o
o PName
pname Diet
d Type
t1 (RetType [TyVar]
ext TypeBase () Freshness
t2))) = do
  t1' <- Type -> SolveM s Type
forall o s. Monoid o => TypeBase () o -> SolveM s (TypeBase () o)
substTyVars Type
t1
  t2' <- substTyVars t2
  pure $
    Scalar $
      Arrow o pname d t1' $
        RetType ext $
          t2' `setMode` freshness t2
substTyVars (Array o
o Shape ()
shape ScalarTypeBase () NoMode
elemt) = do
  elemt' <- Type -> SolveM s Type
forall o s. Monoid o => TypeBase () o -> SolveM s (TypeBase () o)
substTyVars (Type -> SolveM s Type) -> Type -> SolveM s Type
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase () NoMode -> Type
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar ScalarTypeBase () NoMode
elemt
  pure $ arrayOfWithAliases o shape elemt'

occursCheck :: Reason Type -> VName -> VName -> Type -> SolveM s ()
occursCheck :: forall s. Reason Type -> TyVar -> TyVar -> Type -> SolveM s ()
occursCheck Reason Type
reason TyVar
v TyVar
k Type
tp = do
  let vars :: Set TyVar
vars = Type -> Set TyVar
forall dim o. TypeBase dim o -> Set TyVar
typeVars Type
tp
  Bool -> SolveM s () -> SolveM s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TyVar
k TyVar -> Set TyVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set TyVar
vars)
    (SolveM s () -> SolveM s ())
-> (Doc () -> SolveM s ()) -> Doc () -> SolveM s ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError (Reason Type -> Loc
forall a. Located a => a -> Loc
locOf Reason Type
reason) Notes
forall a. Monoid a => a
mempty
    (Doc () -> SolveM s ())
-> (Doc () -> Doc ()) -> Doc () -> SolveM s ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"occurs-check"
    (Doc () -> SolveM s ()) -> Doc () -> SolveM s ()
forall a b. (a -> b) -> a -> b
$ Doc ()
"Occurs check: cannot instantiate"
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TyVar -> Doc ()
forall a. TyVar -> Doc a
forall v a. IsName v => v -> Doc a
prettyName TyVar
v
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"with"
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty Type
tp
      Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

bindTyVar ::
  Reason Type ->
  BreadCrumbs ->
  VName ->
  TyVarNode s ->
  Type ->
  SolveM s ()
bindTyVar :: forall s.
Reason Type
-> BreadCrumbs -> TyVar -> TyVarNode s -> Type -> SolveM s ()
bindTyVar Reason Type
reason BreadCrumbs
bcs TyVar
v TyVarNode s
v_node Type
t' = do
  t <- Type -> SolveM s Type
forall o s. Monoid o => TypeBase () o -> SolveM s (TypeBase () o)
substTyVars Type
t'
  k <- getKey' v_node
  occursCheck reason v k t

  v_info <- getSol' v_node

  setInfo v_node $ Solved t

  case (v_info, t) of
    (Unsolved TyVarFree {}, Type
_) -> () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    (Unsolved (TyVarPrim Loc
_ [PrimType]
v_pts), Type
_) ->
      if Type
t Type -> [Type] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (PrimType -> Type) -> [PrimType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (ScalarTypeBase () NoMode -> Type
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase () NoMode -> Type)
-> (PrimType -> ScalarTypeBase () NoMode) -> PrimType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimType -> ScalarTypeBase () NoMode
forall dim o. PrimType -> ScalarTypeBase dim o
Prim) [PrimType]
v_pts
        then () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        else Reason Type -> Notes -> BreadCrumbs -> Type -> Type -> SolveM s ()
forall s.
Reason Type -> Notes -> BreadCrumbs -> Type -> Type -> SolveM s ()
cannotUnify Reason Type
reason Notes
notes BreadCrumbs
bcs (TyVar -> Type
forall o dim. Monoid o => TyVar -> TypeBase dim o
typeVar TyVar
v) Type
t
      where
        notes :: Notes
notes =
          Doc () -> Notes
aNote (Doc () -> Notes) -> Doc () -> Notes
forall a b. (a -> b) -> a -> b
$
            Doc ()
"Cannot instantiate type that must be one of"
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 ([PrimType] -> Doc ()
forall ann. [PrimType] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
v_pts)
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"with"
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty Type
t)
    (Unsolved (TyVarSum Loc
_ Map Name [Type]
cs1), Scalar (Sum Map Name [Type]
cs2)) ->
      if (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map Name [Type] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [Type]
cs2) (Map Name [Type] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [Type]
cs1)
        then Reason Type
-> BreadCrumbs -> Map Name [Type] -> Map Name [Type] -> SolveM s ()
forall s.
Reason Type
-> BreadCrumbs -> Map Name [Type] -> Map Name [Type] -> SolveM s ()
unifySharedConstructors Reason Type
reason BreadCrumbs
bcs Map Name [Type]
cs1 Map Name [Type]
cs2
        else Reason Type -> Notes -> BreadCrumbs -> Type -> Type -> SolveM s ()
forall s.
Reason Type -> Notes -> BreadCrumbs -> Type -> Type -> SolveM s ()
cannotUnify Reason Type
reason Notes
notes BreadCrumbs
bcs (TyVar -> Type
forall o dim. Monoid o => TyVar -> TypeBase dim o
typeVar TyVar
v) Type
t
      where
        notes :: Notes
notes =
          Doc () -> Notes
aNote (Doc () -> Notes) -> Doc () -> Notes
forall a b. (a -> b) -> a -> b
$
            Doc ()
"Cannot match type with constructors"
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 ([Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
stack ((Name -> Doc ()) -> [Name] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc ()
"#" Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<>) (Doc () -> Doc ()) -> (Name -> Doc ()) -> Name -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty) (Map Name [Type] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [Type]
cs1)))
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"with type with constructors"
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 ([Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
stack ((Name -> Doc ()) -> [Name] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc ()
"#" Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<>) (Doc () -> Doc ()) -> (Name -> Doc ()) -> Name -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty) (Map Name [Type] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [Type]
cs2)))
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Map Name [Type] -> Map Name [Type] -> Doc ()
forall t a. Map Name t -> Map Name t -> Doc a
unsharedConstructorsMsg Map Name [Type]
cs1 Map Name [Type]
cs2
    (Unsolved (TyVarSum Loc
_ Map Name [Type]
cs1), Type
_) ->
      Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError (Reason Type -> Loc
forall a. Located a => a -> Loc
locOf Reason Type
reason) Notes
forall a. Monoid a => a
mempty (Doc () -> SolveM s ()) -> Doc () -> SolveM s ()
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Cannot unify type with constructors"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (ScalarTypeBase () NoMode -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. ScalarTypeBase () NoMode -> Doc ann
pretty (Map Name [Type] -> ScalarTypeBase () NoMode
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum Map Name [Type]
cs1))
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"with type"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty Type
t)
    (Unsolved (TyVarRecord Loc
_ Map Name Type
fs1), Scalar (Record Map Name Type
fs2)) ->
      if (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map Name Type -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name Type
fs2) (Map Name Type -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name Type
fs1)
        then Reason Type
-> BreadCrumbs -> Map Name Type -> Map Name Type -> SolveM s ()
forall s.
Reason Type
-> BreadCrumbs -> Map Name Type -> Map Name Type -> SolveM s ()
unifySharedFields Reason Type
reason BreadCrumbs
bcs Map Name Type
fs1 Map Name Type
fs2
        else
          Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError (Reason Type -> Loc
forall a. Located a => a -> Loc
locOf Reason Type
reason) Notes
forall a. Monoid a => a
mempty (Doc () -> SolveM s ()) -> Doc () -> SolveM s ()
forall a b. (a -> b) -> a -> b
$
            Doc ()
"Cannot unify record type with fields"
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (ScalarTypeBase () NoMode -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. ScalarTypeBase () NoMode -> Doc ann
pretty (Map Name Type -> ScalarTypeBase () NoMode
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record Map Name Type
fs1))
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"with record type"
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (ScalarTypeBase () NoMode -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. ScalarTypeBase () NoMode -> Doc ann
pretty (Map Name Type -> ScalarTypeBase () NoMode
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record Map Name Type
fs2))
    (Unsolved (TyVarRecord Loc
_ Map Name Type
fs1), Type
_) ->
      Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError (Reason Type -> Loc
forall a. Located a => a -> Loc
locOf Reason Type
reason) Notes
forall a. Monoid a => a
mempty (Doc () -> SolveM s ()) -> Doc () -> SolveM s ()
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Cannot unify record type with fields"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (ScalarTypeBase () NoMode -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. ScalarTypeBase () NoMode -> Doc ann
pretty (Map Name Type -> ScalarTypeBase () NoMode
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record Map Name Type
fs1))
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"with type"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty Type
t)
    --
    -- Internal error cases
    (Solved {}, Type
_) ->
      String -> SolveM s ()
forall a. HasCallStack => String -> a
error (String -> SolveM s ()) -> String -> SolveM s ()
forall a b. (a -> b) -> a -> b
$ String
"Type variable already solved: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TyVar -> String
forall v. IsName v => v -> String
prettyNameString TyVar
v
    (Param {}, Type
_) ->
      String -> SolveM s ()
forall a. HasCallStack => String -> a
error (String -> SolveM s ()) -> String -> SolveM s ()
forall a b. (a -> b) -> a -> b
$ String
"Cannot substitute type parameter: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TyVar -> String
forall v. IsName v => v -> String
prettyNameString TyVar
v

solveCt :: CtTy () -> SolveM s ()
solveCt :: forall s. CtTy () -> SolveM s ()
solveCt (CtEq Reason Type
reason Type
t1 Type
t2) = Reason Type -> BreadCrumbs -> Type -> Type -> SolveM s ()
forall s. Reason Type -> BreadCrumbs -> Type -> Type -> SolveM s ()
solveEq Reason Type
reason BreadCrumbs
forall a. Monoid a => a
mempty Type
t1 Type
t2

solveEq :: Reason Type -> BreadCrumbs -> Type -> Type -> SolveM s ()
solveEq :: forall s. Reason Type -> BreadCrumbs -> Type -> Type -> SolveM s ()
solveEq Reason Type
reason BreadCrumbs
obcs Type
orig_t1 Type
orig_t2 = do
  (BreadCrumbs, (Type, Type)) -> SolveM s ()
forall s. (BreadCrumbs, (Type, Type)) -> SolveM s ()
solveCt' (BreadCrumbs
obcs, (Type
orig_t1, Type
orig_t2))
  where
    flexible :: VName -> SolveM s (Maybe (TyVarNode s))
    flexible :: forall s. TyVar -> SolveM s (Maybe (TyVarNode s))
flexible TyVar
v = do
      uf <- (SolverState s -> UF s) -> SolveM s (UF s)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SolverState s -> UF s
forall s. SolverState s -> UF s
solverTyVars
      case M.lookup v uf of
        j_n :: Maybe (TyVarNode s)
j_n@(Just TyVarNode s
node) -> do
          sol <- TyVarNode s -> SolveM s TyVarSol
forall s. TyVarNode s -> SolveM s TyVarSol
getSol' TyVarNode s
node
          pure $ case sol of
            Unsolved TyVarInfo ()
_ -> Maybe (TyVarNode s)
j_n
            TyVarSol
_ -> Maybe (TyVarNode s)
forall a. Maybe a
Nothing
        Maybe (TyVarNode s)
Nothing -> Maybe (TyVarNode s) -> SolveM s (Maybe (TyVarNode s))
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (TyVarNode s)
forall a. Maybe a
Nothing

    normalize :: TypeBase () NoMode -> SolveM s (TypeBase () NoMode)
    normalize :: forall s. Type -> SolveM s Type
normalize t :: Type
t@(Scalar (TypeVar NoMode
_ (QualName [] TyVar
v) [])) = do
      uf <- (SolverState s -> UF s) -> SolveM s (UF s)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SolverState s -> UF s
forall s. SolverState s -> UF s
solverTyVars
      case M.lookup v uf of
        Just TyVarNode s
node -> do
          sol <- TyVarNode s -> SolveM s TyVarSol
forall s. TyVarNode s -> SolveM s TyVarSol
getSol' TyVarNode s
node
          case sol of
            Solved Type
t' -> Type -> SolveM s Type
forall s. Type -> SolveM s Type
normalize Type
t'
            TyVarSol
_ -> TyVar -> Type
forall o dim. Monoid o => TyVar -> TypeBase dim o
typeVar (TyVar -> Type) -> SolveM s TyVar -> SolveM s Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVarNode s -> SolveM s TyVar
forall s. TyVarNode s -> SolveM s TyVar
getKey' TyVarNode s
node
        Maybe (TyVarNode s)
Nothing -> Type -> SolveM s Type
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
    normalize Type
t = Type -> SolveM s Type
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t

    solveCt' :: (BreadCrumbs, (Type, Type)) -> SolveM s ()
    solveCt' :: forall s. (BreadCrumbs, (Type, Type)) -> SolveM s ()
solveCt' (BreadCrumbs
bcs, (Type
t1, Type
t2)) = do
      t1' <- Type -> SolveM s Type
forall s. Type -> SolveM s Type
normalize Type
t1
      t2' <- normalize t2
      case (t1', t2') of
        ( Scalar (TypeVar NoMode
_ (QualName [] TyVar
v1) []),
          Scalar (TypeVar NoMode
_ (QualName [] TyVar
v2) [])
          )
            | TyVar
v1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
v2 -> () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            | Bool
otherwise -> do
                mb_node1 <- TyVar -> SolveM s (Maybe (TyVarNode s))
forall s. TyVar -> SolveM s (Maybe (TyVarNode s))
flexible TyVar
v1
                mb_node2 <- flexible v2
                case (mb_node1, mb_node2) of
                  (Maybe (TyVarNode s)
Nothing, Maybe (TyVarNode s)
Nothing) ->
                    Reason Type -> Notes -> BreadCrumbs -> Type -> Type -> SolveM s ()
forall s.
Reason Type -> Notes -> BreadCrumbs -> Type -> Type -> SolveM s ()
cannotUnify Reason Type
reason Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs Type
t1 Type
t2
                  (Just TyVarNode s
v1_node, Maybe (TyVarNode s)
Nothing) ->
                    Reason Type
-> BreadCrumbs -> TyVar -> TyVarNode s -> Type -> SolveM s ()
forall s.
Reason Type
-> BreadCrumbs -> TyVar -> TyVarNode s -> Type -> SolveM s ()
bindTyVar Reason Type
reason BreadCrumbs
bcs TyVar
v1 TyVarNode s
v1_node Type
t2'
                  (Maybe (TyVarNode s)
Nothing, Just TyVarNode s
v2_node) ->
                    Reason Type
-> BreadCrumbs -> TyVar -> TyVarNode s -> Type -> SolveM s ()
forall s.
Reason Type
-> BreadCrumbs -> TyVar -> TyVarNode s -> Type -> SolveM s ()
bindTyVar Reason Type
reason BreadCrumbs
bcs TyVar
v2 TyVarNode s
v2_node Type
t1'
                  (Just TyVarNode s
v1_node, Just TyVarNode s
v2_node) ->
                    Reason Type
-> BreadCrumbs
-> TyVar
-> TyVarNode s
-> TyVarNode s
-> SolveM s ()
forall s.
Reason Type
-> BreadCrumbs
-> TyVar
-> TyVarNode s
-> TyVarNode s
-> SolveM s ()
unionTyVars Reason Type
reason BreadCrumbs
bcs TyVar
v1 TyVarNode s
v1_node TyVarNode s
v2_node
        (Scalar (TypeVar NoMode
_ (QualName [] TyVar
v1) []), Type
_) -> do
          mb_node <- TyVar -> SolveM s (Maybe (TyVarNode s))
forall s. TyVar -> SolveM s (Maybe (TyVarNode s))
flexible TyVar
v1
          case mb_node of
            Just TyVarNode s
node -> Reason Type
-> BreadCrumbs -> TyVar -> TyVarNode s -> Type -> SolveM s ()
forall s.
Reason Type
-> BreadCrumbs -> TyVar -> TyVarNode s -> Type -> SolveM s ()
bindTyVar Reason Type
reason BreadCrumbs
bcs TyVar
v1 TyVarNode s
node Type
t2'
            Maybe (TyVarNode s)
Nothing -> Type -> Type -> Reason Type -> BreadCrumbs -> SolveM s ()
forall s. Type -> Type -> Reason Type -> BreadCrumbs -> SolveM s ()
tryUnify Type
t1' Type
t2' Reason Type
reason BreadCrumbs
bcs
        (Type
_, Scalar (TypeVar NoMode
_ (QualName [] TyVar
v2) [])) -> do
          mb_node <- TyVar -> SolveM s (Maybe (TyVarNode s))
forall s. TyVar -> SolveM s (Maybe (TyVarNode s))
flexible TyVar
v2
          case mb_node of
            Just TyVarNode s
node -> Reason Type
-> BreadCrumbs -> TyVar -> TyVarNode s -> Type -> SolveM s ()
forall s.
Reason Type
-> BreadCrumbs -> TyVar -> TyVarNode s -> Type -> SolveM s ()
bindTyVar Reason Type
reason BreadCrumbs
bcs TyVar
v2 TyVarNode s
node Type
t1'
            Maybe (TyVarNode s)
Nothing -> Type -> Type -> Reason Type -> BreadCrumbs -> SolveM s ()
forall s. Type -> Type -> Reason Type -> BreadCrumbs -> SolveM s ()
tryUnify Type
t1' Type
t2' Reason Type
reason BreadCrumbs
bcs
        (Type
_, Type
_) -> Type -> Type -> Reason Type -> BreadCrumbs -> SolveM s ()
forall s. Type -> Type -> Reason Type -> BreadCrumbs -> SolveM s ()
tryUnify Type
t1' Type
t2' Reason Type
reason BreadCrumbs
bcs

    tryUnify :: Type -> Type -> Reason Type -> BreadCrumbs -> SolveM s ()
    tryUnify :: forall s. Type -> Type -> Reason Type -> BreadCrumbs -> SolveM s ()
tryUnify Type
t1 Type
t2 Reason Type
r BreadCrumbs
bcs =
      case Type
-> Type -> Either (Maybe (Doc ())) [(BreadCrumbs, (Type, Type))]
forall a.
Type
-> Type -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
unify Type
t1 Type
t2 of
        Left Maybe (Doc ())
details -> Reason Type -> Notes -> BreadCrumbs -> Type -> Type -> SolveM s ()
forall s.
Reason Type -> Notes -> BreadCrumbs -> Type -> Type -> SolveM s ()
cannotUnify Reason Type
r ((Doc () -> Notes) -> Maybe (Doc ()) -> Notes
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Doc () -> Notes
aNote Maybe (Doc ())
details) BreadCrumbs
bcs Type
t1 Type
t2
        Right [(BreadCrumbs, (Type, Type))]
eqs -> ((BreadCrumbs, (Type, Type)) -> SolveM s ())
-> [(BreadCrumbs, (Type, Type))] -> SolveM s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (BreadCrumbs, (Type, Type)) -> SolveM s ()
forall s. (BreadCrumbs, (Type, Type)) -> SolveM s ()
solveCt' [(BreadCrumbs, (Type, Type))]
eqs

-- | Unify at the root, emitting new equalities that must hold.
unify :: Type -> Type -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
unify :: forall a.
Type
-> Type -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
unify (Scalar (Prim PrimType
pt1)) (Scalar (Prim PrimType
pt2))
  | PrimType
pt1 PrimType -> PrimType -> Bool
forall a. Eq a => a -> a -> Bool
== PrimType
pt2 = [(BreadCrumbs, (Type, Type))]
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. b -> Either a b
Right []
unify
  (Scalar (TypeVar NoMode
_ (QualName [TyVar]
_ TyVar
v1) [TypeArg ()]
targs1))
  (Scalar (TypeVar NoMode
_ (QualName [TyVar]
_ TyVar
v2) [TypeArg ()]
targs2))
    | TyVar
v1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
v2 =
        [(BreadCrumbs, (Type, Type))]
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. b -> Either a b
Right ([(BreadCrumbs, (Type, Type))]
 -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
-> [(BreadCrumbs, (Type, Type))]
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. (a -> b) -> a -> b
$ ((TypeArg (), TypeArg ()) -> Maybe (BreadCrumbs, (Type, Type)))
-> [(TypeArg (), TypeArg ())] -> [(BreadCrumbs, (Type, Type))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TypeArg (), TypeArg ()) -> Maybe (BreadCrumbs, (Type, Type))
forall {a} {dim} {dim}.
Monoid a =>
(TypeArg dim, TypeArg dim)
-> Maybe (a, (TypeBase dim NoMode, TypeBase dim NoMode))
f ([(TypeArg (), TypeArg ())] -> [(BreadCrumbs, (Type, Type))])
-> [(TypeArg (), TypeArg ())] -> [(BreadCrumbs, (Type, Type))]
forall a b. (a -> b) -> a -> b
$ [TypeArg ()] -> [TypeArg ()] -> [(TypeArg (), TypeArg ())]
forall a b. [a] -> [b] -> [(a, b)]
zip [TypeArg ()]
targs1 [TypeArg ()]
targs2
    where
      f :: (TypeArg dim, TypeArg dim)
-> Maybe (a, (TypeBase dim NoMode, TypeBase dim NoMode))
f (TypeArgType TypeBase dim NoMode
t1, TypeArgType TypeBase dim NoMode
t2) = (a, (TypeBase dim NoMode, TypeBase dim NoMode))
-> Maybe (a, (TypeBase dim NoMode, TypeBase dim NoMode))
forall a. a -> Maybe a
Just (a
forall a. Monoid a => a
mempty, (TypeBase dim NoMode
t1, TypeBase dim NoMode
t2))
      f (TypeArg dim, TypeArg dim)
_ = Maybe (a, (TypeBase dim NoMode, TypeBase dim NoMode))
forall a. Maybe a
Nothing
unify
  (Scalar (Arrow NoMode
_ PName
_ Diet
_ Type
t1a (RetType [TyVar]
_ TypeBase () Freshness
t1r)))
  (Scalar (Arrow NoMode
_ PName
_ Diet
_ Type
t2a (RetType [TyVar]
_ TypeBase () Freshness
t2r))) =
    [(BreadCrumbs, (Type, Type))]
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. b -> Either a b
Right [(BreadCrumbs
forall a. Monoid a => a
mempty, (Type
t1a, Type
t2a)), (BreadCrumbs
forall a. Monoid a => a
mempty, (Type
t1r', Type
t2r'))]
    where
      t1r' :: Type
t1r' = TypeBase () Freshness
t1r TypeBase () Freshness -> NoMode -> Type
forall dim o1 o2. TypeBase dim o1 -> o2 -> TypeBase dim o2
`setMode` NoMode
NoMode
      t2r' :: Type
t2r' = TypeBase () Freshness
t2r TypeBase () Freshness -> NoMode -> Type
forall dim o1 o2. TypeBase dim o1 -> o2 -> TypeBase dim o2
`setMode` NoMode
NoMode
unify (Scalar (Record Map Name Type
fs1)) (Scalar (Record Map Name Type
fs2))
  | Map Name Type -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name Type
fs1 [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== Map Name Type -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name Type
fs2 =
      [(BreadCrumbs, (Type, Type))]
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. b -> Either a b
Right ([(BreadCrumbs, (Type, Type))]
 -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
-> [(BreadCrumbs, (Type, Type))]
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. (a -> b) -> a -> b
$
        ((Name, (Type, Type)) -> (BreadCrumbs, (Type, Type)))
-> [(Name, (Type, Type))] -> [(BreadCrumbs, (Type, Type))]
forall a b. (a -> b) -> [a] -> [b]
map ((Name -> BreadCrumbs)
-> (Name, (Type, Type)) -> (BreadCrumbs, (Type, Type))
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Name -> BreadCrumbs
matchingField) ([(Name, (Type, Type))] -> [(BreadCrumbs, (Type, Type))])
-> [(Name, (Type, Type))] -> [(BreadCrumbs, (Type, Type))]
forall a b. (a -> b) -> a -> b
$
          Map Name (Type, Type) -> [(Name, (Type, Type))]
forall k a. Map k a -> [(k, a)]
M.toList (Map Name (Type, Type) -> [(Name, (Type, Type))])
-> Map Name (Type, Type) -> [(Name, (Type, Type))]
forall a b. (a -> b) -> a -> b
$
            (Type -> Type -> (Type, Type))
-> Map Name Type -> Map Name Type -> Map Name (Type, Type)
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map Name Type
fs1 Map Name Type
fs2
  | Just Level
n1 <- [Type] -> Level
forall a. [a] -> Level
forall (t :: * -> *) a. Foldable t => t a -> Level
length ([Type] -> Level) -> Maybe [Type] -> Maybe Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name Type -> Maybe [Type]
forall a. Map Name a -> Maybe [a]
areTupleFields Map Name Type
fs1,
    Just Level
n2 <- [Type] -> Level
forall a. [a] -> Level
forall (t :: * -> *) a. Foldable t => t a -> Level
length ([Type] -> Level) -> Maybe [Type] -> Maybe Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name Type -> Maybe [Type]
forall a. Map Name a -> Maybe [a]
areTupleFields Map Name Type
fs2,
    Level
n1 Level -> Level -> Bool
forall a. Eq a => a -> a -> Bool
/= Level
n2 =
      Maybe (Doc a)
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. a -> Either a b
Left (Maybe (Doc a)
 -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
-> (Doc a -> Maybe (Doc a))
-> Doc a
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc a -> Maybe (Doc a)
forall a. a -> Maybe a
Just (Doc a -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
-> Doc a -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. (a -> b) -> a -> b
$
        Doc a
"Tuples have"
          Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Level -> Doc a
forall ann. Level -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Level
n1
          Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc a
"and"
          Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Level -> Doc a
forall ann. Level -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Level
n2
          Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc a
"elements respectively."
  | Bool
otherwise =
      let missing :: [Name]
missing =
            (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Map Name Type -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name Type
fs1) (Map Name Type -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name Type
fs2)
              [Name] -> [Name] -> [Name]
forall a. Semigroup a => a -> a -> a
<> (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Map Name Type -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name Type
fs2) (Map Name Type -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name Type
fs1)
       in Maybe (Doc a)
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. a -> Either a b
Left (Maybe (Doc a)
 -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
-> (Doc a -> Maybe (Doc a))
-> Doc a
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc a -> Maybe (Doc a)
forall a. a -> Maybe a
Just (Doc a -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
-> Doc a -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. (a -> b) -> a -> b
$
            Doc a
"unshared fields:" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc a] -> Doc a
forall a. [Doc a] -> Doc a
commasep ((Name -> Doc a) -> [Name] -> [Doc a]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty [Name]
missing) Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<> Doc a
"."
unify (Scalar (Sum Map Name [Type]
cs1)) (Scalar (Sum Map Name [Type]
cs2))
  | Map Name [Type] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [Type]
cs1 [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== Map Name [Type] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [Type]
cs2 =
      ([[(BreadCrumbs, (Type, Type))]] -> [(BreadCrumbs, (Type, Type))])
-> Either (Maybe (Doc a)) [[(BreadCrumbs, (Type, Type))]]
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b.
(a -> b) -> Either (Maybe (Doc a)) a -> Either (Maybe (Doc a)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[(BreadCrumbs, (Type, Type))]] -> [(BreadCrumbs, (Type, Type))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Either (Maybe (Doc a)) [[(BreadCrumbs, (Type, Type))]]
 -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
-> (((Name, ([Type], [Type]))
     -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
    -> Either (Maybe (Doc a)) [[(BreadCrumbs, (Type, Type))]])
-> ((Name, ([Type], [Type]))
    -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, ([Type], [Type]))]
-> ((Name, ([Type], [Type]))
    -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
-> Either (Maybe (Doc a)) [[(BreadCrumbs, (Type, Type))]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, ([Type], [Type]))]
cs' (((Name, ([Type], [Type]))
  -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
 -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
-> ((Name, ([Type], [Type]))
    -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. (a -> b) -> a -> b
$ \(Name
c, ([Type]
ts1, [Type]
ts2)) -> do
        if [Type] -> Level
forall a. [a] -> Level
forall (t :: * -> *) a. Foldable t => t a -> Level
length [Type]
ts1 Level -> Level -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Level
forall a. [a] -> Level
forall (t :: * -> *) a. Foldable t => t a -> Level
length [Type]
ts2
          then [(BreadCrumbs, (Type, Type))]
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. b -> Either a b
Right ([(BreadCrumbs, (Type, Type))]
 -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
-> [(BreadCrumbs, (Type, Type))]
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> (BreadCrumbs, (Type, Type)))
-> [Type] -> [Type] -> [(BreadCrumbs, (Type, Type))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (((Type, Type) -> (BreadCrumbs, (Type, Type)))
-> Type -> Type -> (BreadCrumbs, (Type, Type))
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Name -> BreadCrumbs
matchingConstructor Name
c,)) [Type]
ts1 [Type]
ts2
          else Maybe (Doc a)
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. a -> Either a b
Left Maybe (Doc a)
forall a. Maybe a
Nothing
  | Bool
otherwise =
      Maybe (Doc a)
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. a -> Either a b
Left (Maybe (Doc a)
 -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
-> (Doc a -> Maybe (Doc a))
-> Doc a
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc a -> Maybe (Doc a)
forall a. a -> Maybe a
Just (Doc a -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))])
-> Doc a -> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. (a -> b) -> a -> b
$ Map Name [Type] -> Map Name [Type] -> Doc a
forall t a. Map Name t -> Map Name t -> Doc a
unsharedConstructorsMsg Map Name [Type]
cs1 Map Name [Type]
cs2
  where
    cs' :: [(Name, ([Type], [Type]))]
cs' = Map Name ([Type], [Type]) -> [(Name, ([Type], [Type]))]
forall k a. Map k a -> [(k, a)]
M.toList (Map Name ([Type], [Type]) -> [(Name, ([Type], [Type]))])
-> Map Name ([Type], [Type]) -> [(Name, ([Type], [Type]))]
forall a b. (a -> b) -> a -> b
$ ([Type] -> [Type] -> ([Type], [Type]))
-> Map Name [Type] -> Map Name [Type] -> Map Name ([Type], [Type])
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map Name [Type]
cs1 Map Name [Type]
cs2
unify Type
t1 Type
t2
  | Just Type
t1' <- Level -> Type -> Maybe Type
forall dim o. Level -> TypeBase dim o -> Maybe (TypeBase dim o)
peelArray Level
1 Type
t1,
    Just Type
t2' <- Level -> Type -> Maybe Type
forall dim o. Level -> TypeBase dim o -> Maybe (TypeBase dim o)
peelArray Level
1 Type
t2 =
      [(BreadCrumbs, (Type, Type))]
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. b -> Either a b
Right [(BreadCrumbs
forall a. Monoid a => a
mempty, (Type
t1', Type
t2'))]
unify Type
_ Type
_ = Maybe (Doc a)
-> Either (Maybe (Doc a)) [(BreadCrumbs, (Type, Type))]
forall a b. a -> Either a b
Left Maybe (Doc a)
forall a. Maybe a
Nothing

maybeLookupTyVarSol :: TyVar -> SolveM s (Maybe TyVarSol)
maybeLookupTyVarSol :: forall s. TyVar -> SolveM s (Maybe TyVarSol)
maybeLookupTyVarSol TyVar
tv = do
  tyvars <- (SolverState s -> UF s) -> SolveM s (UF s)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SolverState s -> UF s
forall s. SolverState s -> UF s
solverTyVars
  case M.lookup tv tyvars of
    Maybe (TyVarNode s)
Nothing -> Maybe TyVarSol -> SolveM s (Maybe TyVarSol)
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe TyVarSol
forall a. Maybe a
Nothing
    Just TyVarNode s
node -> do
      sol <- TyVarNode s -> SolveM s TyVarSol
forall s. TyVarNode s -> SolveM s TyVarSol
getSol' TyVarNode s
node
      pure $ Just sol

lookupTyVar :: TyVar -> SolveM s (Either (TyVarInfo ()) Type)
lookupTyVar :: forall s. TyVar -> SolveM s (Either (TyVarInfo ()) Type)
lookupTyVar TyVar
tv =
  Either (TyVarInfo ()) Type
-> (TyVarSol -> Either (TyVarInfo ()) Type)
-> Maybe TyVarSol
-> Either (TyVarInfo ()) Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Either (TyVarInfo ()) Type
forall {b}. b
bad TyVarSol -> Either (TyVarInfo ()) Type
unpack (Maybe TyVarSol -> Either (TyVarInfo ()) Type)
-> SolveM s (Maybe TyVarSol)
-> SolveM s (Either (TyVarInfo ()) Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVar -> SolveM s (Maybe TyVarSol)
forall s. TyVar -> SolveM s (Maybe TyVarSol)
maybeLookupTyVarSol TyVar
tv
  where
    bad :: b
bad = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ String
"Unknown tyvar: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TyVar -> String
forall v. IsName v => v -> String
prettyNameString TyVar
tv
    unpack :: TyVarSol -> Either (TyVarInfo ()) Type
unpack (Param {}) = String -> Either (TyVarInfo ()) Type
forall a. HasCallStack => String -> a
error (String -> Either (TyVarInfo ()) Type)
-> String -> Either (TyVarInfo ()) Type
forall a b. (a -> b) -> a -> b
$ String
"Is a type param: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TyVar -> String
forall v. IsName v => v -> String
prettyNameString TyVar
tv
    unpack (Solved Type
t) = Type -> Either (TyVarInfo ()) Type
forall a b. b -> Either a b
Right Type
t
    unpack (Unsolved TyVarInfo ()
info) = TyVarInfo () -> Either (TyVarInfo ()) Type
forall a b. a -> Either a b
Left TyVarInfo ()
info

lookupTyVarInfo :: TyVarNode s -> SolveM s (TyVarInfo ())
lookupTyVarInfo :: forall s. TyVarNode s -> SolveM s (TyVarInfo ())
lookupTyVarInfo TyVarNode s
v_node = do
  r <- TyVarNode s -> SolveM s TyVarSol
forall s. TyVarNode s -> SolveM s TyVarSol
getSol' TyVarNode s
v_node
  case r of
    Unsolved TyVarInfo ()
info -> TyVarInfo () -> SolveM s (TyVarInfo ())
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TyVarInfo ()
info
    TyVarSol
_ -> do
      v <- TyVarNode s -> SolveM s TyVar
forall s. TyVarNode s -> SolveM s TyVar
getKey' TyVarNode s
v_node
      error $ "Tyvar is nonflexible: " <> prettyNameString v

lookupUF :: TyVar -> SolveM s (TyVarNode s)
lookupUF :: forall s. TyVar -> SolveM s (TyVarNode s)
lookupUF TyVar
tv = do
  uf <- (SolverState s -> UF s) -> SolveM s (UF s)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SolverState s -> UF s
forall s. SolverState s -> UF s
solverTyVars
  case M.lookup tv uf of
    Maybe (TyVarNode s)
Nothing -> String -> SolveM s (TyVarNode s)
forall a. HasCallStack => String -> a
error (String -> SolveM s (TyVarNode s))
-> String -> SolveM s (TyVarNode s)
forall a b. (a -> b) -> a -> b
$ String
"Unknown tyvar: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TyVar -> String
forall v. IsName v => v -> String
prettyNameString TyVar
tv
    Just TyVarNode s
node -> TyVarNode s -> SolveM s (TyVarNode s)
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TyVarNode s
node

unifySharedFields ::
  Reason Type ->
  BreadCrumbs ->
  M.Map Name Type ->
  M.Map Name Type ->
  SolveM s ()
unifySharedFields :: forall s.
Reason Type
-> BreadCrumbs -> Map Name Type -> Map Name Type -> SolveM s ()
unifySharedFields Reason Type
reason BreadCrumbs
bcs Map Name Type
fs1 Map Name Type
fs2 =
  [(Name, (Type, Type))]
-> ((Name, (Type, Type)) -> SolveM s ()) -> SolveM s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Name (Type, Type) -> [(Name, (Type, Type))]
forall k a. Map k a -> [(k, a)]
M.toList (Map Name (Type, Type) -> [(Name, (Type, Type))])
-> Map Name (Type, Type) -> [(Name, (Type, Type))]
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> (Type, Type))
-> Map Name Type -> Map Name Type -> Map Name (Type, Type)
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map Name Type
fs1 Map Name Type
fs2) (((Name, (Type, Type)) -> SolveM s ()) -> SolveM s ())
-> ((Name, (Type, Type)) -> SolveM s ()) -> SolveM s ()
forall a b. (a -> b) -> a -> b
$ \(Name
f, (Type
ts1, Type
ts2)) ->
    Reason Type -> BreadCrumbs -> Type -> Type -> SolveM s ()
forall s. Reason Type -> BreadCrumbs -> Type -> Type -> SolveM s ()
solveEq Reason Type
reason (Name -> BreadCrumbs
matchingField Name
f BreadCrumbs -> BreadCrumbs -> BreadCrumbs
forall a. Semigroup a => a -> a -> a
<> BreadCrumbs
bcs) Type
ts1 Type
ts2

unifySharedConstructors ::
  Reason Type ->
  BreadCrumbs ->
  M.Map Name [Type] ->
  M.Map Name [Type] ->
  SolveM s ()
unifySharedConstructors :: forall s.
Reason Type
-> BreadCrumbs -> Map Name [Type] -> Map Name [Type] -> SolveM s ()
unifySharedConstructors Reason Type
reason BreadCrumbs
bcs Map Name [Type]
cs1 Map Name [Type]
cs2 =
  [(Name, ([Type], [Type]))]
-> ((Name, ([Type], [Type])) -> SolveM s ()) -> SolveM s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Name ([Type], [Type]) -> [(Name, ([Type], [Type]))]
forall k a. Map k a -> [(k, a)]
M.toList (Map Name ([Type], [Type]) -> [(Name, ([Type], [Type]))])
-> Map Name ([Type], [Type]) -> [(Name, ([Type], [Type]))]
forall a b. (a -> b) -> a -> b
$ ([Type] -> [Type] -> ([Type], [Type]))
-> Map Name [Type] -> Map Name [Type] -> Map Name ([Type], [Type])
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map Name [Type]
cs1 Map Name [Type]
cs2) (((Name, ([Type], [Type])) -> SolveM s ()) -> SolveM s ())
-> ((Name, ([Type], [Type])) -> SolveM s ()) -> SolveM s ()
forall a b. (a -> b) -> a -> b
$ \(Name
c, ([Type]
ts1, [Type]
ts2)) ->
    if [Type] -> Level
forall a. [a] -> Level
forall (t :: * -> *) a. Foldable t => t a -> Level
length [Type]
ts1 Level -> Level -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Level
forall a. [a] -> Level
forall (t :: * -> *) a. Foldable t => t a -> Level
length [Type]
ts2
      then (Type -> Type -> SolveM s ()) -> [Type] -> [Type] -> SolveM s ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (Reason Type -> BreadCrumbs -> Type -> Type -> SolveM s ()
forall s. Reason Type -> BreadCrumbs -> Type -> Type -> SolveM s ()
solveEq Reason Type
reason (BreadCrumbs -> Type -> Type -> SolveM s ())
-> BreadCrumbs -> Type -> Type -> SolveM s ()
forall a b. (a -> b) -> a -> b
$ Name -> BreadCrumbs
matchingConstructor Name
c BreadCrumbs -> BreadCrumbs -> BreadCrumbs
forall a. Semigroup a => a -> a -> a
<> BreadCrumbs
bcs) [Type]
ts1 [Type]
ts2
      else
        Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError (Reason Type -> Loc
forall a. Located a => a -> Loc
locOf Reason Type
reason) Notes
forall a. Monoid a => a
mempty (Doc () -> SolveM s ()) -> Doc () -> SolveM s ()
forall a b. (a -> b) -> a -> b
$
          Doc ()
"Cannot unify type with constructor"
            Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (ScalarTypeBase () NoMode -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. ScalarTypeBase () NoMode -> Doc ann
pretty (Map Name [Type] -> ScalarTypeBase () NoMode
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum (Name -> [Type] -> Map Name [Type]
forall k a. k -> a -> Map k a
M.singleton Name
c [Type]
ts1)))
            Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"with type of constructor"
            Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (ScalarTypeBase () NoMode -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. ScalarTypeBase () NoMode -> Doc ann
pretty (Map Name [Type] -> ScalarTypeBase () NoMode
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum (Name -> [Type] -> Map Name [Type]
forall k a. k -> a -> Map k a
M.singleton Name
c [Type]
ts2)))
            Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"because they differ in arity."

setInfo :: TyVarNode s -> TyVarSol -> SolveM s ()
setInfo :: forall s. TyVarNode s -> TyVarSol -> SolveM s ()
setInfo TyVarNode s
node TyVarSol
sol = ST s () -> SolveM s ()
forall s a. ST s a -> SolveM s a
liftST (ST s () -> SolveM s ()) -> ST s () -> SolveM s ()
forall a b. (a -> b) -> a -> b
$ TyVarNode s -> TyVarSol -> ST s ()
forall s. TyVarNode s -> TyVarSol -> ST s ()
assignNewSol TyVarNode s
node TyVarSol
sol

unionTyVars ::
  Reason Type ->
  BreadCrumbs ->
  VName ->
  TyVarNode s ->
  TyVarNode s ->
  SolveM s ()
unionTyVars :: forall s.
Reason Type
-> BreadCrumbs
-> TyVar
-> TyVarNode s
-> TyVarNode s
-> SolveM s ()
unionTyVars Reason Type
reason BreadCrumbs
bcs TyVar
v TyVarNode s
v_node TyVarNode s
t_node = do
  v_sol <- TyVarNode s -> SolveM s TyVarSol
forall s. TyVarNode s -> SolveM s TyVarSol
getSol' TyVarNode s
v_node
  t_info <- lookupTyVarInfo t_node
  c <- check v_sol t_info
  case c of
    Left (Loc
loc, Notes
notes, Doc ()
msg) -> Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError Loc
loc Notes
notes Doc ()
msg
    Right (Just TyVarSol
new_sol) -> TyVarNode s -> TyVarNode s -> TyVarSol -> SolveM s ()
forall s. TyVarNode s -> TyVarNode s -> TyVarSol -> SolveM s ()
unionNewSol' TyVarNode s
v_node TyVarNode s
t_node TyVarSol
new_sol
    Right Maybe TyVarSol
Nothing -> TyVarNode s -> TyVarNode s -> SolveM s ()
forall s. TyVarNode s -> TyVarNode s -> SolveM s ()
union' TyVarNode s
v_node TyVarNode s
t_node
  where
    check ::
      TyVarSol ->
      TyVarInfo () ->
      SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
    check :: forall s.
TyVarSol
-> TyVarInfo ()
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
check TyVarSol
v_sol TyVarInfo ()
t_info =
      case (TyVarSol
v_sol, TyVarInfo ()
t_info) of
        (Unsolved (TyVarFree Loc
_ Liftedness
v_l), TyVarFree Loc
t_loc Liftedness
t_l)
          | Liftedness
v_l Liftedness -> Liftedness -> Bool
forall a. Eq a => a -> a -> Bool
/= Liftedness
t_l ->
              Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
 -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)))
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a b. (a -> b) -> a -> b
$ Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. b -> Either a b
Right (Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
-> Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. (a -> b) -> a -> b
$ TyVarSol -> Maybe TyVarSol
forall a. a -> Maybe a
Just (TyVarSol -> Maybe TyVarSol) -> TyVarSol -> Maybe TyVarSol
forall a b. (a -> b) -> a -> b
$ TyVarInfo () -> TyVarSol
Unsolved (TyVarInfo () -> TyVarSol) -> TyVarInfo () -> TyVarSol
forall a b. (a -> b) -> a -> b
$ Loc -> Liftedness -> TyVarInfo ()
forall d. Loc -> Liftedness -> TyVarInfo d
TyVarFree Loc
t_loc (Liftedness -> Liftedness -> Liftedness
forall a. Ord a => a -> a -> a
min Liftedness
v_l Liftedness
t_l)
        (Unsolved TyVarInfo ()
info, TyVarFree {}) -> do
          Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
 -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)))
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a b. (a -> b) -> a -> b
$ Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. b -> Either a b
Right (Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
-> Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. (a -> b) -> a -> b
$ TyVarSol -> Maybe TyVarSol
forall a. a -> Maybe a
Just (TyVarSol -> Maybe TyVarSol) -> TyVarSol -> Maybe TyVarSol
forall a b. (a -> b) -> a -> b
$ TyVarInfo () -> TyVarSol
Unsolved TyVarInfo ()
info
        --
        -- TyVarPrim cases
        ( Unsolved (TyVarPrim Loc
_ [PrimType]
v_pts),
          TyVarPrim Loc
t_loc [PrimType]
t_pts
          ) ->
            let pts :: [PrimType]
pts = [PrimType] -> [PrimType] -> [PrimType]
forall a. Eq a => [a] -> [a] -> [a]
L.intersect [PrimType]
v_pts [PrimType]
t_pts
             in case [PrimType]
pts of
                  [] ->
                    Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
 -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)))
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a b. (a -> b) -> a -> b
$
                      (Loc, Notes, Doc ())
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. a -> Either a b
Left
                        ( Reason Type -> Loc
forall a. Located a => a -> Loc
locOf Reason Type
reason,
                          Notes
forall a. Monoid a => a
mempty,
                          Doc ()
"Cannot unify type that must be one of"
                            Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 ([PrimType] -> Doc ()
forall ann. [PrimType] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
v_pts)
                            Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"with type that must be one of"
                            Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 ([PrimType] -> Doc ()
forall ann. [PrimType] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
t_pts)
                        )
                  [PrimType]
_ -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
 -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)))
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a b. (a -> b) -> a -> b
$ Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. b -> Either a b
Right (Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
-> Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. (a -> b) -> a -> b
$ TyVarSol -> Maybe TyVarSol
forall a. a -> Maybe a
Just (TyVarSol -> Maybe TyVarSol) -> TyVarSol -> Maybe TyVarSol
forall a b. (a -> b) -> a -> b
$ TyVarInfo () -> TyVarSol
Unsolved (TyVarInfo () -> TyVarSol) -> TyVarInfo () -> TyVarSol
forall a b. (a -> b) -> a -> b
$ Loc -> [PrimType] -> TyVarInfo ()
forall d. Loc -> [PrimType] -> TyVarInfo d
TyVarPrim Loc
t_loc [PrimType]
pts
        (Unsolved (TyVarPrim Loc
_ [PrimType]
v_pts), TyVarRecord {}) ->
          Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
 -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)))
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a b. (a -> b) -> a -> b
$
            (Loc, Notes, Doc ())
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. a -> Either a b
Left
              ( Reason Type -> Loc
forall a. Located a => a -> Loc
locOf Reason Type
reason,
                Notes
forall a. Monoid a => a
mempty,
                Doc ()
"Cannot unify type that must be one of"
                  Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 ([PrimType] -> Doc ()
forall ann. [PrimType] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
v_pts)
                  Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"with type that must be a record."
              )
        (Unsolved (TyVarPrim Loc
_ [PrimType]
v_pts), TyVarSum {}) ->
          Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
 -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)))
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a b. (a -> b) -> a -> b
$
            (Loc, Notes, Doc ())
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. a -> Either a b
Left
              ( Reason Type -> Loc
forall a. Located a => a -> Loc
locOf Reason Type
reason,
                Notes
forall a. Monoid a => a
mempty,
                Doc ()
"Cannot unify type that must be one of"
                  Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 ([PrimType] -> Doc ()
forall ann. [PrimType] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
v_pts)
                  Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"with type that must be sum."
              )
        --
        -- TyVarSum cases
        ( Unsolved (TyVarSum Loc
_ Map Name [Type]
cs1),
          TyVarSum Loc
loc Map Name [Type]
cs2
          ) -> do
            Reason Type
-> BreadCrumbs -> Map Name [Type] -> Map Name [Type] -> SolveM s ()
forall s.
Reason Type
-> BreadCrumbs -> Map Name [Type] -> Map Name [Type] -> SolveM s ()
unifySharedConstructors Reason Type
reason BreadCrumbs
bcs Map Name [Type]
cs1 Map Name [Type]
cs2
            let cs3 :: Map Name [Type]
cs3 = Map Name [Type]
cs1 Map Name [Type] -> Map Name [Type] -> Map Name [Type]
forall a. Semigroup a => a -> a -> a
<> Map Name [Type]
cs2
            Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
 -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)))
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a b. (a -> b) -> a -> b
$ Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. b -> Either a b
Right (Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
-> Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. (a -> b) -> a -> b
$ TyVarSol -> Maybe TyVarSol
forall a. a -> Maybe a
Just (TyVarSol -> Maybe TyVarSol) -> TyVarSol -> Maybe TyVarSol
forall a b. (a -> b) -> a -> b
$ TyVarInfo () -> TyVarSol
Unsolved (TyVarInfo () -> TyVarSol) -> TyVarInfo () -> TyVarSol
forall a b. (a -> b) -> a -> b
$ Loc -> Map Name [Type] -> TyVarInfo ()
forall d. Loc -> Map Name [CtType d] -> TyVarInfo d
TyVarSum Loc
loc Map Name [Type]
cs3
        ( Unsolved TyVarSum {},
          TyVarPrim Loc
_ [PrimType]
pts
          ) ->
            Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
 -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)))
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a b. (a -> b) -> a -> b
$
              (Loc, Notes, Doc ())
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. a -> Either a b
Left
                ( Reason Type -> Loc
forall a. Located a => a -> Loc
locOf Reason Type
reason,
                  Notes
forall a. Monoid a => a
mempty,
                  Doc ()
"A sum type cannot be one of"
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 ([PrimType] -> Doc ()
forall ann. [PrimType] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
pts)
                )
        ( Unsolved (TyVarSum Loc
_ Map Name [Type]
cs1),
          TyVarRecord Loc
_ Map Name Type
fs
          ) ->
            Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
 -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)))
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a b. (a -> b) -> a -> b
$
              (Loc, Notes, Doc ())
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. a -> Either a b
Left
                ( Reason Type -> Loc
forall a. Located a => a -> Loc
locOf Reason Type
reason,
                  Notes
forall a. Monoid a => a
mempty,
                  Doc ()
"Cannot unify type with constructors"
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (ScalarTypeBase () NoMode -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. ScalarTypeBase () NoMode -> Doc ann
pretty (Map Name [Type] -> ScalarTypeBase () NoMode
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum Map Name [Type]
cs1))
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"with type"
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty (ScalarTypeBase () NoMode -> Type
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (Map Name Type -> ScalarTypeBase () NoMode
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record Map Name Type
fs)))
                )
        --
        -- TyVarRecord cases
        ( Unsolved (TyVarRecord Loc
_ Map Name Type
fs1),
          TyVarRecord Loc
loc Map Name Type
fs2
          ) -> do
            Reason Type
-> BreadCrumbs -> Map Name Type -> Map Name Type -> SolveM s ()
forall s.
Reason Type
-> BreadCrumbs -> Map Name Type -> Map Name Type -> SolveM s ()
unifySharedFields Reason Type
reason BreadCrumbs
bcs Map Name Type
fs1 Map Name Type
fs2
            let fs3 :: Map Name Type
fs3 = Map Name Type
fs1 Map Name Type -> Map Name Type -> Map Name Type
forall a. Semigroup a => a -> a -> a
<> Map Name Type
fs2
            Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
 -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)))
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a b. (a -> b) -> a -> b
$ Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. b -> Either a b
Right (Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
-> Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. (a -> b) -> a -> b
$ TyVarSol -> Maybe TyVarSol
forall a. a -> Maybe a
Just (TyVarSol -> Maybe TyVarSol) -> TyVarSol -> Maybe TyVarSol
forall a b. (a -> b) -> a -> b
$ TyVarInfo () -> TyVarSol
Unsolved (TyVarInfo () -> TyVarSol) -> TyVarInfo () -> TyVarSol
forall a b. (a -> b) -> a -> b
$ Loc -> Map Name Type -> TyVarInfo ()
forall d. Loc -> Map Name (CtType d) -> TyVarInfo d
TyVarRecord Loc
loc Map Name Type
fs3
        ( Unsolved TyVarRecord {},
          TyVarPrim Loc
_ [PrimType]
pts
          ) ->
            Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
 -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)))
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a b. (a -> b) -> a -> b
$
              (Loc, Notes, Doc ())
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. a -> Either a b
Left
                ( Reason Type -> Loc
forall a. Located a => a -> Loc
locOf Reason Type
reason,
                  Notes
forall a. Monoid a => a
mempty,
                  Doc ()
"A record type cannot be one of"
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 ([PrimType] -> Doc ()
forall ann. [PrimType] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
pts)
                )
        ( Unsolved (TyVarRecord Loc
_ Map Name Type
fs1),
          TyVarSum Loc
_ Map Name [Type]
cs
          ) ->
            Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
 -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)))
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a b. (a -> b) -> a -> b
$
              (Loc, Notes, Doc ())
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. a -> Either a b
Left
                ( Reason Type -> Loc
forall a. Located a => a -> Loc
locOf Reason Type
reason,
                  Notes
forall a. Monoid a => a
mempty,
                  Doc ()
"Cannot unify record type"
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (ScalarTypeBase () NoMode -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. ScalarTypeBase () NoMode -> Doc ann
pretty (Map Name Type -> ScalarTypeBase () NoMode
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record Map Name Type
fs1))
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"with type"
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty (ScalarTypeBase () NoMode -> Type
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (Map Name [Type] -> ScalarTypeBase () NoMode
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum Map Name [Type]
cs)))
                )
        --
        -- Internal error cases
        (Solved {}, TyVarInfo ()
_) -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall {b}. b
alreadySolved
        (Param {}, TyVarInfo ()
_) -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall {b}. b
isParam
        (TyVarSol, TyVarInfo ())
_ -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
 -> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol)))
-> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
-> SolveM s (Either (Loc, Notes, Doc ()) (Maybe TyVarSol))
forall a b. (a -> b) -> a -> b
$ Maybe TyVarSol -> Either (Loc, Notes, Doc ()) (Maybe TyVarSol)
forall a b. b -> Either a b
Right Maybe TyVarSol
forall a. Maybe a
Nothing

    alreadySolved :: b
alreadySolved = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ String
"Type variable already solved: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TyVar -> String
forall v. IsName v => v -> String
prettyNameString TyVar
v
    isParam :: b
isParam = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ String
"Type name is a type parameter: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TyVar -> String
forall v. IsName v => v -> String
prettyNameString TyVar
v

scopeViolation :: Reason Type -> VName -> Type -> VName -> SolveM s ()
scopeViolation :: forall s. Reason Type -> TyVar -> Type -> TyVar -> SolveM s ()
scopeViolation Reason Type
reason TyVar
v1 Type
ty TyVar
v2 =
  Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError (Reason Type -> Loc
forall a. Located a => a -> Loc
locOf Reason Type
reason) Notes
forall a. Monoid a => a
mempty (Doc () -> SolveM s ())
-> (Doc () -> Doc ()) -> Doc () -> SolveM s ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"scope-violation" (Doc () -> SolveM s ()) -> Doc () -> SolveM s ()
forall a b. (a -> b) -> a -> b
$
    Doc ()
"Cannot unify type"
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty Type
ty)
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"with"
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (TyVar -> Doc ()
forall a. TyVar -> Doc a
forall v a. IsName v => v -> Doc a
prettyName TyVar
v1)
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"(scope violation)."
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"This is because"
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (TyVar -> Doc ()
forall a. TyVar -> Doc a
forall v a. IsName v => v -> Doc a
prettyName TyVar
v2)
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"is rigidly bound in a deeper scope."

scopeCheck :: Reason Type -> TyVar -> Level -> Type -> SolveM s ()
scopeCheck :: forall s. Reason Type -> TyVar -> Level -> Type -> SolveM s ()
scopeCheck Reason Type
reason TyVar
v Level
v_lvl Type
ty = (TyVar -> SolveM s ()) -> Set TyVar -> SolveM s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TyVar -> SolveM s ()
forall s. TyVar -> SolveM s ()
check (Set TyVar -> SolveM s ()) -> Set TyVar -> SolveM s ()
forall a b. (a -> b) -> a -> b
$ Type -> Set TyVar
forall dim o. TypeBase dim o -> Set TyVar
typeVars Type
ty
  where
    check :: TyVar -> SolveM s ()
    check :: forall s. TyVar -> SolveM s ()
check TyVar
ty_v = do
      SolveM s ()
-> (TyVarNode s -> SolveM s ())
-> Maybe (TyVarNode s)
-> SolveM s ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) TyVarNode s -> SolveM s ()
forall s. TyVarNode s -> SolveM s ()
checkNode (Maybe (TyVarNode s) -> SolveM s ())
-> SolveM s (Maybe (TyVarNode s)) -> SolveM s ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TyVar -> SolveM s (Maybe (TyVarNode s))
forall s. TyVar -> SolveM s (Maybe (TyVarNode s))
maybeLookupUF TyVar
ty_v

    checkNode :: TyVarNode s -> SolveM s ()
    checkNode :: forall s. TyVarNode s -> SolveM s ()
checkNode TyVarNode s
node = do
      sol <- TyVarNode s -> SolveM s TyVarSol
forall s. TyVarNode s -> SolveM s TyVarSol
getSol' TyVarNode s
node
      case sol of
        Param Level
ty_v_lvl Liftedness
_ Loc
_
          | Level
ty_v_lvl Level -> Level -> Bool
forall a. Ord a => a -> a -> Bool
> Level
v_lvl -> do
              k <- TyVarNode s -> SolveM s TyVar
forall s. TyVarNode s -> SolveM s TyVar
getKey' TyVarNode s
node
              ty' <- substTyVars ty
              scopeViolation reason v ty' k
        Solved Type
ty' -> do
          (TyVar -> SolveM s ()) -> Set TyVar -> SolveM s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TyVar -> SolveM s ()
forall s. TyVar -> SolveM s ()
check (Set TyVar -> SolveM s ()) -> Set TyVar -> SolveM s ()
forall a b. (a -> b) -> a -> b
$ Type -> Set TyVar
forall dim o. TypeBase dim o -> Set TyVar
typeVars Type
ty'
        TyVarSol
_ -> () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | If a type variable has a liftedness constraint, we propagate that
-- constraint to its solution. The actual checking for correct usage
-- is done later, by 'localChecks' and 'instTyVars' in the sized type
-- checker, which know why the constraints exist and can produce
-- proper error messages.
liftednessCheck :: Liftedness -> Type -> SolveM s ()
liftednessCheck :: forall s. Liftedness -> Type -> SolveM s ()
liftednessCheck Liftedness
l (Scalar (TypeVar NoMode
_ (QualName [] TyVar
v) [TypeArg ()]
_)) = do
  v_info <- TyVar -> SolveM s (Maybe TyVarSol)
forall s. TyVar -> SolveM s (Maybe TyVarSol)
maybeLookupTyVarSol TyVar
v
  case v_info of
    Maybe TyVarSol
Nothing ->
      -- Is an opaque type.
      () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Just (Solved Type
v_ty) ->
      Liftedness -> Type -> SolveM s ()
forall s. Liftedness -> Type -> SolveM s ()
liftednessCheck Liftedness
l Type
v_ty
    Just Param {} -> () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Just (Unsolved (TyVarFree Loc
loc Liftedness
v_l))
      | Liftedness
l Liftedness -> Liftedness -> Bool
forall a. Ord a => a -> a -> Bool
< Liftedness
v_l -> do
          node <- TyVar -> SolveM s (TyVarNode s)
forall s. TyVar -> SolveM s (TyVarNode s)
lookupUF TyVar
v
          setInfo node $ Unsolved $ TyVarFree loc l
    Just Unsolved {} -> () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
liftednessCheck Liftedness
_ (Scalar Prim {}) = () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
liftednessCheck Liftedness
Lifted Type
_ = () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
liftednessCheck Liftedness
_ Array {} = () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
liftednessCheck Liftedness
_ (Scalar Arrow {}) = () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
liftednessCheck Liftedness
l (Scalar (Record Map Name Type
fs)) =
  (Type -> SolveM s ()) -> Map Name Type -> SolveM s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Liftedness -> Type -> SolveM s ()
forall s. Liftedness -> Type -> SolveM s ()
liftednessCheck Liftedness
l) Map Name Type
fs
liftednessCheck Liftedness
l (Scalar (Sum Map Name [Type]
cs)) =
  ([Type] -> SolveM s ()) -> Map Name [Type] -> SolveM s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Type -> SolveM s ()) -> [Type] -> SolveM s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Type -> SolveM s ()) -> [Type] -> SolveM s ())
-> (Type -> SolveM s ()) -> [Type] -> SolveM s ()
forall a b. (a -> b) -> a -> b
$ Liftedness -> Type -> SolveM s ()
forall s. Liftedness -> Type -> SolveM s ()
liftednessCheck Liftedness
l) Map Name [Type]
cs
liftednessCheck Liftedness
_ (Scalar TypeVar {}) = () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

solveTyVar :: (VName, (Level, TyVarInfo ())) -> SolveM s ()
solveTyVar :: forall s. (TyVar, (Level, TyVarInfo ())) -> SolveM s ()
solveTyVar (TyVar
tv, (Level
lvl, TyVarFree Loc
loc Liftedness
l)) = do
  tv_t <- TyVar -> SolveM s (Either (TyVarInfo ()) Type)
forall s. TyVar -> SolveM s (Either (TyVarInfo ()) Type)
lookupTyVar TyVar
tv
  case tv_t of
    Right Type
ty -> do
      Reason Type -> TyVar -> Level -> Type -> SolveM s ()
forall s. Reason Type -> TyVar -> Level -> Type -> SolveM s ()
scopeCheck (Loc -> Reason Type
forall t. Loc -> Reason t
Reason Loc
loc) TyVar
tv Level
lvl Type
ty
      Liftedness -> Type -> SolveM s ()
forall s. Liftedness -> Type -> SolveM s ()
liftednessCheck Liftedness
l Type
ty
    Either (TyVarInfo ()) Type
_ -> () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
solveTyVar (TyVar
tv, (Level
_, TyVarPrim Loc
loc [PrimType]
pts)) = do
  tv_t <- TyVar -> SolveM s (Either (TyVarInfo ()) Type)
forall s. TyVar -> SolveM s (Either (TyVarInfo ()) Type)
lookupTyVar TyVar
tv
  case tv_t of
    Right Type
ty
      | Type
ty Type -> [Type] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (PrimType -> Type) -> [PrimType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (ScalarTypeBase () NoMode -> Type
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase () NoMode -> Type)
-> (PrimType -> ScalarTypeBase () NoMode) -> PrimType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimType -> ScalarTypeBase () NoMode
forall dim o. PrimType -> ScalarTypeBase dim o
Prim) [PrimType]
pts -> () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      | Bool
otherwise ->
          Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> SolveM s ()) -> Doc () -> SolveM s ()
forall a b. (a -> b) -> a -> b
$
            Doc ()
"Numeric constant inferred to be of type"
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
align (Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty Type
ty))
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"which is not possible."
    Either (TyVarInfo ()) Type
_ -> () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
solveTyVar (TyVar
tv, (Level
_, TyVarRecord Loc
loc Map Name Type
fs1)) = do
  tv_t <- TyVar -> SolveM s (Either (TyVarInfo ()) Type)
forall s. TyVar -> SolveM s (Either (TyVarInfo ()) Type)
lookupTyVar TyVar
tv
  case tv_t of
    Left TyVarInfo ()
_ ->
      Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> SolveM s ())
-> (Doc () -> Doc ()) -> Doc () -> SolveM s ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"ambiguous-type" (Doc () -> SolveM s ()) -> Doc () -> SolveM s ()
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TyVar -> Doc ()
forall a. TyVar -> Doc a
forall v a. IsName v => v -> Doc a
prettyName TyVar
tv
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"is ambiguous."
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Must be a record with fields"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty (ScalarTypeBase () NoMode -> Type
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (Map Name Type -> ScalarTypeBase () NoMode
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record Map Name Type
fs1)))
    Right Type
_ -> () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
solveTyVar (TyVar
tv, (Level
_, TyVarSum Loc
loc Map Name [Type]
cs1)) = do
  tv_t <- TyVar -> SolveM s (Either (TyVarInfo ()) Type)
forall s. TyVar -> SolveM s (Either (TyVarInfo ()) Type)
lookupTyVar TyVar
tv
  case tv_t of
    Left TyVarInfo ()
_ ->
      Loc -> Notes -> Doc () -> SolveM s ()
forall s. Loc -> Notes -> Doc () -> SolveM s ()
typeError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> SolveM s ())
-> (Doc () -> Doc ()) -> Doc () -> SolveM s ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"ambiguous-type" (Doc () -> SolveM s ()) -> Doc () -> SolveM s ()
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type is ambiguous."
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Must be a sum type with constructors"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Level -> Doc () -> Doc ()
forall ann. Level -> Doc ann -> Doc ann
indent Level
2 (Type -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Type -> Doc ann
pretty (ScalarTypeBase () NoMode -> Type
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (Map Name [Type] -> ScalarTypeBase () NoMode
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum Map Name [Type]
cs1)))
    Right Type
_ -> () -> SolveM s ()
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

maybeLookupUF :: TyVar -> SolveM s (Maybe (TyVarNode s))
maybeLookupUF :: forall s. TyVar -> SolveM s (Maybe (TyVarNode s))
maybeLookupUF TyVar
tv = do
  uf <- (SolverState s -> UF s) -> SolveM s (UF s)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SolverState s -> UF s
forall s. SolverState s -> UF s
solverTyVars
  pure . M.lookup tv $ uf

getSolution :: SolveM s ([UnconTyVar], Solution)
getSolution :: forall s. SolveM s ([UnconTyVar], Solution)
getSolution = do
  uf <- (SolverState s -> UF s) -> SolveM s (UF s)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SolverState s -> UF s
forall s. SolverState s -> UF s
solverTyVars
  resolved <- M.traverseWithKey resolve uf
  let unconstrained = (TyVar
 -> (Either [PrimType] Type, Maybe Liftedness)
 -> [UnconTyVar]
 -> [UnconTyVar])
-> [UnconTyVar]
-> Map TyVar (Either [PrimType] Type, Maybe Liftedness)
-> [UnconTyVar]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey TyVar
-> (Either [PrimType] Type, Maybe Liftedness)
-> [UnconTyVar]
-> [UnconTyVar]
unconstr [] Map TyVar (Either [PrimType] Type, Maybe Liftedness)
resolved
      sol = (TyVar
 -> (Either [PrimType] Type, Maybe Liftedness)
 -> Maybe (Either [PrimType] Type))
-> Map TyVar (Either [PrimType] Type, Maybe Liftedness) -> Solution
forall k a b. (k -> a -> Maybe b) -> Map k a -> Map k b
M.mapMaybeWithKey TyVar
-> (Either [PrimType] Type, Maybe Liftedness)
-> Maybe (Either [PrimType] Type)
mkSubst Map TyVar (Either [PrimType] Type, Maybe Liftedness)
resolved
  pure (unconstrained, sol)
  where
    resolve ::
      TyVar ->
      TyVarNode s ->
      SolveM s (Either [PrimType] (TypeBase () NoMode), Maybe Liftedness)
    resolve :: forall s.
TyVar
-> TyVarNode s
-> SolveM s (Either [PrimType] Type, Maybe Liftedness)
resolve TyVar
tv TyVarNode s
node = do
      sol <- TyVarNode s -> SolveM s TyVarSol
forall s. TyVarNode s -> SolveM s TyVarSol
getSol' TyVarNode s
node
      case sol of
        Unsolved (TyVarFree Loc
_ Liftedness
l) -> do
          k <- TyVarNode s -> SolveM s TyVar
forall s. TyVarNode s -> SolveM s TyVar
getKey' TyVarNode s
node
          let tv' = TyVar -> TypeBase dim NoMode
forall o dim. Monoid o => TyVar -> TypeBase dim o
typeVar TyVar
k
          -- If the current type variable and root type variable are
          -- different, this variable is unconstrained, so we save the
          -- liftedness constraint for later.
          pure (Right tv', if k == tv then Just l else Nothing)
        Unsolved (TyVarPrim Loc
_ [PrimType]
pts) -> (Either [PrimType] Type, Maybe Liftedness)
-> SolveM s (Either [PrimType] Type, Maybe Liftedness)
forall a. a -> SolveM s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([PrimType] -> Either [PrimType] Type
forall a b. a -> Either a b
Left [PrimType]
pts, Maybe Liftedness
forall a. Maybe a
Nothing)
        Solved Type
t -> do
          t' <- Type -> SolveM s Type
forall o s. Monoid o => TypeBase () o -> SolveM s (TypeBase () o)
substTyVars Type
t
          pure (Right $ first (const ()) t', Nothing)
        TyVarSol
_ -> do
          k <- TyVarNode s -> SolveM s TyVar
forall s. TyVarNode s -> SolveM s TyVar
getKey' TyVarNode s
node
          pure (Right $ typeVar k, Nothing)

    unconstr ::
      TyVar ->
      (Either [PrimType] (TypeBase () NoMode), Maybe Liftedness) ->
      [UnconTyVar] ->
      [UnconTyVar]
    unconstr :: TyVar
-> (Either [PrimType] Type, Maybe Liftedness)
-> [UnconTyVar]
-> [UnconTyVar]
unconstr TyVar
tv (Either [PrimType] Type
_, Just Liftedness
l) [UnconTyVar]
acc = (TyVar
tv, Liftedness
l) UnconTyVar -> [UnconTyVar] -> [UnconTyVar]
forall a. a -> [a] -> [a]
: [UnconTyVar]
acc
    unconstr TyVar
_ (Either [PrimType] Type, Maybe Liftedness)
_ [UnconTyVar]
acc = [UnconTyVar]
acc

    mkSubst ::
      TyVar ->
      (Either [PrimType] (TypeBase () NoMode), Maybe Liftedness) ->
      Maybe (Either [PrimType] (TypeBase () NoMode))
    mkSubst :: TyVar
-> (Either [PrimType] Type, Maybe Liftedness)
-> Maybe (Either [PrimType] Type)
mkSubst TyVar
_ (Either [PrimType] Type
_, Just Liftedness
_) = Maybe (Either [PrimType] Type)
forall a. Maybe a
Nothing
    mkSubst TyVar
tv (s :: Either [PrimType] Type
s@(Right (Scalar (TypeVar NoMode
_ (QualName [] TyVar
tv') [TypeArg ()]
_))), Maybe Liftedness
_) =
      if TyVar
tv TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
/= TyVar
tv' then Either [PrimType] Type -> Maybe (Either [PrimType] Type)
forall a. a -> Maybe a
Just Either [PrimType] Type
s else Maybe (Either [PrimType] Type)
forall a. Maybe a
Nothing
    mkSubst TyVar
_ (Either [PrimType] Type
s, Maybe Liftedness
_) = Either [PrimType] Type -> Maybe (Either [PrimType] Type)
forall a. a -> Maybe a
Just Either [PrimType] Type
s

-- | Solve type constraints, producing either an error or a solution,
-- alongside a list of unconstrained type variables.
solve ::
  [CtTy ()] ->
  TyParams ->
  TyVars () ->
  Either TypeError ([UnconTyVar], Solution)
solve :: [CtTy ()]
-> TyParams
-> TyVars ()
-> Either TypeError ([UnconTyVar], Solution)
solve [CtTy ()]
constraints TyParams
typarams TyVars ()
tyvars =
  (forall s. ST s (Either TypeError ([UnconTyVar], Solution)))
-> Either TypeError ([UnconTyVar], Solution)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (Either TypeError ([UnconTyVar], Solution)))
 -> Either TypeError ([UnconTyVar], Solution))
-> (forall s. ST s (Either TypeError ([UnconTyVar], Solution)))
-> Either TypeError ([UnconTyVar], Solution)
forall a b. (a -> b) -> a -> b
$ do
    r <- TyParams -> TyVars () -> ST s (SolverState s)
forall s. TyParams -> TyVars () -> ST s (SolverState s)
initializeState TyParams
typarams TyVars ()
tyvars
    flip runReaderT r $ runExceptT $ runSolveM $ do
      mapM_ solveCt constraints
      mapM_ solveTyVar $ M.toList tyvars
      getSolution
{-# NOINLINE solve #-}