{-# LANGUAGE DuplicateRecordFields #-}

-- |
-- Interaction solver for Coercible constraints
--
module Language.PureScript.TypeChecker.Entailment.Coercible
  ( GivenSolverState(..)
  , initialGivenSolverState
  , solveGivens
  , WantedSolverState(..)
  , initialWantedSolverState
  , solveWanteds
  , insoluble
  ) where

import Prelude hiding (interact)

import Control.Applicative ((<|>), empty)
import Control.Arrow ((&&&))
import Control.Monad ((<=<), guard, unless, when)
import Control.Monad.Error.Class (MonadError, catchError, throwError)
import Control.Monad.State (MonadState, StateT, get, gets, modify, put)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Maybe (MaybeT(..), runMaybeT)
import Control.Monad.Trans.Except (ExceptT(..), runExceptT)
import Control.Monad.Writer.Strict (MonadWriter, Writer, execWriter, runWriter, runWriterT, tell)
import Data.Either (partitionEithers)
import Data.Foldable (fold, foldl', for_, toList)
import Data.Functor (($>))
import Data.List (find)
import Data.Maybe (fromMaybe, isJust)
import Data.Monoid (Any(..))
import Data.Text (Text)

import qualified Data.Map as M
import qualified Data.Set as S

import Language.PureScript.Crash
import Language.PureScript.Environment
import Language.PureScript.Errors hiding (inScope)
import Language.PureScript.Names
import Language.PureScript.TypeChecker.Kinds hiding (kindOf)
import Language.PureScript.TypeChecker.Monad
import Language.PureScript.TypeChecker.Roles
import Language.PureScript.TypeChecker.Synonyms
import Language.PureScript.TypeChecker.Unify
import Language.PureScript.Roles
import Language.PureScript.Types
import qualified Language.PureScript.Constants.Prim as Prim

-- | State of the given constraints solver.
data GivenSolverState =
  GivenSolverState
    { GivenSolverState -> [(SourceType, SourceType, SourceType)]
inertGivens :: [(SourceType, SourceType, SourceType)]
  -- ^ A set of irreducible given constraints which do not interact together.
    , GivenSolverState -> [(SourceType, SourceType)]
unsolvedGivens :: [(SourceType, SourceType)]
  -- ^ Given constraints yet to be solved.
    }

-- | Initialize the given constraints solver state with the givens to solve.
initialGivenSolverState :: [(SourceType, SourceType)] -> GivenSolverState
initialGivenSolverState :: [(SourceType, SourceType)] -> GivenSolverState
initialGivenSolverState =
  [(SourceType, SourceType, SourceType)]
-> [(SourceType, SourceType)] -> GivenSolverState
GivenSolverState []

-- | The given constraints solver follows these steps:
--
-- 1. Solving can diverge for recursive newtypes, so we check the solver depth
-- and abort if we crossed an arbitrary limit.
--
-- For instance the declarations:
--
-- @
-- newtype N a = N (a -> N a)
--
-- example :: forall a b. N a -> N b
-- example = coerce
-- @
--
-- yield the wanted @Coercible (N a) (N b)@ which we can unwrap on both sides
-- to yield @Coercible (a -> N a) (b -> N b)@, which we can then decompose back
-- to @Coercible a b@ and @Coercible (N a) (N b)@.
--
-- 2. We pick a constraint from the unsolved queue. If the queue is empty we are
-- done, otherwise we unify the constraint arguments kinds and continue.
--
-- 3. Then we try to canonicalize the constraint.

-- 3a. Canonicalization can fail, in which case we swallow the error and pretend
-- the constraint is irreducible because it is possible to eventually solve it.
--
-- For instance the declarations:
--
-- @
-- data D a = D a
-- type role D nominal
--
-- example :: forall a b. Coercible (D a) (D b) => D a -> D b
-- example = coerce
-- @
--
-- yield an insoluble given @Coercible (D a) (D b)@ which discharges the wanted
-- constraint regardless, because the given can be solved if @a@ and @b@ turn
-- out to be equal: @example (D true) :: D Boolean@ should compile.
--
-- 3b. Canonicalization can succeed with an irreducible constraint which we
-- then interact with the inert set.
--
-- 3bi. These interactions can yield a derived constraint which we add to the
-- unsolved queue and then go back to 1.
--
-- 3bii. These interactions can discharge the constraint, in which case we go
-- back to 1.
--
-- 3biii The constraint may not react to the inert set, in which case we add it
-- to the inert set, kick out any constraint that can be rewritten by the new
-- inert, add them to the unsolved queue and then go back to 1.
--
-- 3c. Otherwise canonicalization can succeed with derived constraints which we
-- add to the unsolved queue and then go back to 1.
solveGivens
  :: MonadError MultipleErrors m
  => MonadState CheckState m
  => Environment
  -> StateT GivenSolverState m ()
solveGivens :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Environment -> StateT GivenSolverState m ()
solveGivens Environment
env = Int -> StateT GivenSolverState m ()
go (Int
0 :: Int) where
  go :: Int -> StateT GivenSolverState m ()
go Int
n = do
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n forall a. Ord a => a -> a -> Bool
> Int
1000) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ SimpleErrorMessage
PossiblyInfiniteCoercibleInstance
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets GivenSolverState -> [(SourceType, SourceType)]
unsolvedGivens forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      (SourceType, SourceType)
given : [(SourceType, SourceType)]
unsolved -> do
        (SourceType
k, SourceType
a, SourceType
b) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
(SourceType, SourceType) -> m (SourceType, SourceType, SourceType)
unify (SourceType, SourceType)
given
        GivenSolverState{[(SourceType, SourceType)]
[(SourceType, SourceType, SourceType)]
unsolvedGivens :: [(SourceType, SourceType)]
inertGivens :: [(SourceType, SourceType, SourceType)]
$sel:unsolvedGivens:GivenSolverState :: GivenSolverState -> [(SourceType, SourceType)]
$sel:inertGivens:GivenSolverState :: GivenSolverState -> [(SourceType, SourceType, SourceType)]
..} <- forall s (m :: * -> *). MonadState s m => m s
get
        forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (forall (m :: * -> *).
(MonadError MultipleErrors m, MonadWriter [ErrorMessageHint] m,
 MonadState CheckState m) =>
Environment
-> Maybe [(SourceType, SourceType, SourceType)]
-> SourceType
-> SourceType
-> SourceType
-> m Canonicalized
canon Environment
env forall a. Maybe a
Nothing SourceType
k SourceType
a SourceType
b forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall {f :: * -> *} {p}. Applicative f => p -> f Canonicalized
recover)) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Canonicalized
Irreducible -> case Environment
-> (SourceType, SourceType)
-> [(SourceType, SourceType, SourceType)]
-> Maybe Interaction
interact Environment
env (SourceType
a, SourceType
b) [(SourceType, SourceType, SourceType)]
inertGivens of
            Just (Simplified (SourceType
a', SourceType
b')) ->
              forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ GivenSolverState { $sel:unsolvedGivens:GivenSolverState :: [(SourceType, SourceType)]
unsolvedGivens = (SourceType
a', SourceType
b') forall a. a -> [a] -> [a]
: [(SourceType, SourceType)]
unsolved, [(SourceType, SourceType, SourceType)]
inertGivens :: [(SourceType, SourceType, SourceType)]
$sel:inertGivens:GivenSolverState :: [(SourceType, SourceType, SourceType)]
.. }
            Just Interaction
Discharged ->
              forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ GivenSolverState { $sel:unsolvedGivens:GivenSolverState :: [(SourceType, SourceType)]
unsolvedGivens = [(SourceType, SourceType)]
unsolved, [(SourceType, SourceType, SourceType)]
inertGivens :: [(SourceType, SourceType, SourceType)]
$sel:inertGivens:GivenSolverState :: [(SourceType, SourceType, SourceType)]
.. }
            Maybe Interaction
Nothing -> do
              let ([(SourceType, SourceType)]
kickedOut, [(SourceType, SourceType, SourceType)]
kept) = forall a b. [Either a b] -> ([a], [b])
partitionEithers forall a b. (a -> b) -> a -> b
$ Environment
-> (SourceType, SourceType)
-> (SourceType, SourceType, SourceType)
-> Either
     (SourceType, SourceType) (SourceType, SourceType, SourceType)
kicksOut Environment
env (SourceType
a, SourceType
b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SourceType, SourceType, SourceType)]
inertGivens
              forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ GivenSolverState
                { $sel:inertGivens:GivenSolverState :: [(SourceType, SourceType, SourceType)]
inertGivens = (SourceType
k, SourceType
a, SourceType
b) forall a. a -> [a] -> [a]
: [(SourceType, SourceType, SourceType)]
kept
                , $sel:unsolvedGivens:GivenSolverState :: [(SourceType, SourceType)]
unsolvedGivens = [(SourceType, SourceType)]
kickedOut forall a. Semigroup a => a -> a -> a
<> [(SourceType, SourceType)]
unsolved
                }
          Canonicalized Set (SourceType, SourceType)
deriveds ->
            forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ GivenSolverState { $sel:unsolvedGivens:GivenSolverState :: [(SourceType, SourceType)]
unsolvedGivens = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Set (SourceType, SourceType)
deriveds forall a. Semigroup a => a -> a -> a
<> [(SourceType, SourceType)]
unsolved, [(SourceType, SourceType, SourceType)]
inertGivens :: [(SourceType, SourceType, SourceType)]
$sel:inertGivens:GivenSolverState :: [(SourceType, SourceType, SourceType)]
.. }
        Int -> StateT GivenSolverState m ()
go (Int
n forall a. Num a => a -> a -> a
+ Int
1)
  recover :: p -> f Canonicalized
recover p
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure Canonicalized
Irreducible

-- | State of the wanted constraints solver.
data WantedSolverState =
  WantedSolverState
    { WantedSolverState -> [(SourceType, SourceType, SourceType)]
inertGivens :: [(SourceType, SourceType, SourceType)]
  -- ^ A set of irreducible given constraints which do not interact together,
  -- but which could interact with the wanteds.
    , WantedSolverState -> [(SourceType, SourceType, SourceType)]
inertWanteds :: [(SourceType, SourceType, SourceType)]
  -- ^ A set of irreducible wanted constraints which do not interact together,
  -- nor with any given.
    , WantedSolverState -> [(SourceType, SourceType)]
unsolvedWanteds :: [(SourceType, SourceType)]
  -- ^ Wanted constraints yet to be solved.
    }

-- | Initialize the wanted constraints solver state with an inert set of givens
-- and the two parameters of the wanted to solve.
initialWantedSolverState
  :: [(SourceType, SourceType, SourceType)]
  -> SourceType
  -> SourceType
  -> WantedSolverState
initialWantedSolverState :: [(SourceType, SourceType, SourceType)]
-> SourceType -> SourceType -> WantedSolverState
initialWantedSolverState [(SourceType, SourceType, SourceType)]
givens SourceType
a SourceType
b =
  [(SourceType, SourceType, SourceType)]
-> [(SourceType, SourceType, SourceType)]
-> [(SourceType, SourceType)]
-> WantedSolverState
WantedSolverState [(SourceType, SourceType, SourceType)]
givens [] [(SourceType
a, SourceType
b)]

-- | The wanted constraints solver follows similar steps than the given solver,
-- except for:
--
-- 1. When canonicalization fails we can swallow the error, but only if the
-- wanted interacts with the givens.
--
-- For instance the declarations:
--
-- @
-- data D a = D a
-- type role D nominal
--
-- example :: forall a b. Coercible (D a) (D b) => D a -> D b
-- example = coerce
-- @
--
-- yield an insoluble wanted @Coercible (D a) (D b)@ which is discharged by
-- the given. But we want @example :: forall a b. D a -> D b@ to fail.
--
-- 2. Irreducible wanted constraints don't interact with the inert wanteds set,
-- because doing so would yield confusing error messages.
--
-- For instance the declarations:
--
-- @
-- data D a = D a
--
-- example :: forall a. D a a -> D Boolean Char
-- example = coerce
-- @
--
-- yield the wanted @Coercible (D a a) (D Boolean Char)@, which is decomposed to
-- the irreducibles @Coercible a Boolean@ and @Coercible a Char@. Would we
-- interact the latter with the former, we would report an insoluble
-- @Coercible Boolean Char@.
solveWanteds
  :: MonadError MultipleErrors m
  => MonadWriter [ErrorMessageHint] m
  => MonadState CheckState m
  => Environment
  -> StateT WantedSolverState m ()
solveWanteds :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadWriter [ErrorMessageHint] m,
 MonadState CheckState m) =>
Environment -> StateT WantedSolverState m ()
solveWanteds Environment
env = Int -> StateT WantedSolverState m ()
go (Int
0 :: Int) where
  go :: Int -> StateT WantedSolverState m ()
go Int
n = do
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n forall a. Ord a => a -> a -> Bool
> Int
1000) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ SimpleErrorMessage
PossiblyInfiniteCoercibleInstance
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets WantedSolverState -> [(SourceType, SourceType)]
unsolvedWanteds forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      (SourceType, SourceType)
wanted : [(SourceType, SourceType)]
unsolved -> do
        (SourceType
k, SourceType
a, SourceType
b) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
(SourceType, SourceType) -> m (SourceType, SourceType, SourceType)
unify (SourceType, SourceType)
wanted
        WantedSolverState{[(SourceType, SourceType)]
[(SourceType, SourceType, SourceType)]
unsolvedWanteds :: [(SourceType, SourceType)]
inertWanteds :: [(SourceType, SourceType, SourceType)]
inertGivens :: [(SourceType, SourceType, SourceType)]
$sel:unsolvedWanteds:WantedSolverState :: WantedSolverState -> [(SourceType, SourceType)]
$sel:inertWanteds:WantedSolverState :: WantedSolverState -> [(SourceType, SourceType, SourceType)]
$sel:inertGivens:WantedSolverState :: WantedSolverState -> [(SourceType, SourceType, SourceType)]
..} <- forall s (m :: * -> *). MonadState s m => m s
get
        forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall (m :: * -> *).
(MonadError MultipleErrors m, MonadWriter [ErrorMessageHint] m,
 MonadState CheckState m) =>
Environment
-> Maybe [(SourceType, SourceType, SourceType)]
-> SourceType
-> SourceType
-> SourceType
-> m Canonicalized
canon Environment
env (forall a. a -> Maybe a
Just [(SourceType, SourceType, SourceType)]
inertGivens) SourceType
k SourceType
a SourceType
b forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` (SourceType, SourceType)
-> [(SourceType, SourceType, SourceType)]
-> MultipleErrors
-> m Canonicalized
recover (SourceType
a, SourceType
b) [(SourceType, SourceType, SourceType)]
inertGivens) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Canonicalized
Irreducible -> case Environment
-> (SourceType, SourceType)
-> [(SourceType, SourceType, SourceType)]
-> Maybe Interaction
interact Environment
env (SourceType
a, SourceType
b) [(SourceType, SourceType, SourceType)]
inertGivens of
            Just (Simplified (SourceType
a', SourceType
b')) ->
              forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ WantedSolverState { $sel:unsolvedWanteds:WantedSolverState :: [(SourceType, SourceType)]
unsolvedWanteds = (SourceType
a', SourceType
b') forall a. a -> [a] -> [a]
: [(SourceType, SourceType)]
unsolved, [(SourceType, SourceType, SourceType)]
inertWanteds :: [(SourceType, SourceType, SourceType)]
inertGivens :: [(SourceType, SourceType, SourceType)]
$sel:inertWanteds:WantedSolverState :: [(SourceType, SourceType, SourceType)]
$sel:inertGivens:WantedSolverState :: [(SourceType, SourceType, SourceType)]
.. }
            Just Interaction
Discharged ->
              forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ WantedSolverState { $sel:unsolvedWanteds:WantedSolverState :: [(SourceType, SourceType)]
unsolvedWanteds = [(SourceType, SourceType)]
unsolved, [(SourceType, SourceType, SourceType)]
inertWanteds :: [(SourceType, SourceType, SourceType)]
inertGivens :: [(SourceType, SourceType, SourceType)]
$sel:inertWanteds:WantedSolverState :: [(SourceType, SourceType, SourceType)]
$sel:inertGivens:WantedSolverState :: [(SourceType, SourceType, SourceType)]
.. }
            Maybe Interaction
Nothing ->
              forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ WantedSolverState
                { $sel:inertWanteds:WantedSolverState :: [(SourceType, SourceType, SourceType)]
inertWanteds = (SourceType
k, SourceType
a, SourceType
b) forall a. a -> [a] -> [a]
: [(SourceType, SourceType, SourceType)]
inertWanteds
                , $sel:unsolvedWanteds:WantedSolverState :: [(SourceType, SourceType)]
unsolvedWanteds = [(SourceType, SourceType)]
unsolved
                , [(SourceType, SourceType, SourceType)]
inertGivens :: [(SourceType, SourceType, SourceType)]
$sel:inertGivens:WantedSolverState :: [(SourceType, SourceType, SourceType)]
..
                }
          Canonicalized Set (SourceType, SourceType)
deriveds ->
            forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ WantedSolverState { $sel:unsolvedWanteds:WantedSolverState :: [(SourceType, SourceType)]
unsolvedWanteds = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Set (SourceType, SourceType)
deriveds forall a. Semigroup a => a -> a -> a
<> [(SourceType, SourceType)]
unsolved, [(SourceType, SourceType, SourceType)]
inertWanteds :: [(SourceType, SourceType, SourceType)]
inertGivens :: [(SourceType, SourceType, SourceType)]
$sel:inertWanteds:WantedSolverState :: [(SourceType, SourceType, SourceType)]
$sel:inertGivens:WantedSolverState :: [(SourceType, SourceType, SourceType)]
.. }
        Int -> StateT WantedSolverState m ()
go (Int
n forall a. Num a => a -> a -> a
+ Int
1)
  recover :: (SourceType, SourceType)
-> [(SourceType, SourceType, SourceType)]
-> MultipleErrors
-> m Canonicalized
recover (SourceType, SourceType)
wanted [(SourceType, SourceType, SourceType)]
givens MultipleErrors
errors =
    case Environment
-> (SourceType, SourceType)
-> [(SourceType, SourceType, SourceType)]
-> Maybe Interaction
interact Environment
env (SourceType, SourceType)
wanted [(SourceType, SourceType, SourceType)]
givens of
      Maybe Interaction
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError MultipleErrors
errors
      Just (Simplified (SourceType, SourceType)
wanted') -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (SourceType, SourceType) -> Canonicalized
Canonicalized forall a b. (a -> b) -> a -> b
$ forall a. a -> Set a
S.singleton (SourceType, SourceType)
wanted'
      Just Interaction
Discharged -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Set (SourceType, SourceType) -> Canonicalized
Canonicalized forall a. Monoid a => a
mempty

-- | Unifying constraints arguments kinds isn't strictly necessary but yields
-- better error messages. For instance we cannot solve the constraint
-- @Coercible (D :: Type -> Type) (D a :: Type)@ because its arguments kinds
-- don't match and trying to unify them will say so, which is more helpful than
-- simply saying that no type class instance was found.
--
-- A subtle thing to note is that types with polymorphic kinds can be annotated
-- with kind applications mentioning unknowns that we may have solved by
-- unifying the kinds.
--
-- For instance the declarations:
--
-- @
-- data D :: forall k. k -> Type
-- data D a = D
--
-- type role D representational
--
-- example :: D D -> D D
-- example = coerce
-- @
--
-- yield a wanted
-- @Coercible (D \@(k1 -> Type) (D \@k1)) (D \@(k2 -> Type) (D \@k2))@, which we
-- decompose to @Coercible (D \@k1) (D \@k2)@, where @k1@ and @k2@ are unknowns.
-- This constraint is not reflexive because @D \@k1@ and @D \@k2@ are differents
-- but both arguments kinds unify with @k -> Type@, where @k@ is a fresh unknown,
-- so applying the substitution to @D \@k1@ and @D \@k2@ yields a
-- @Coercible (D \@k) (D \@k)@ constraint which could be trivially solved by
-- reflexivity instead of having to saturate the type constructors.
unify
  :: MonadError MultipleErrors m
  => MonadState CheckState m
  => (SourceType, SourceType)
  -> m (SourceType, SourceType, SourceType)
unify :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
(SourceType, SourceType) -> m (SourceType, SourceType, SourceType)
unify (SourceType
a, SourceType
b) = do
  let kindOf :: SourceType -> m (SourceType, SourceType)
kindOf = forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> a
id forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> m SourceType
elaborateKind) forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms
  (SourceType
a', SourceType
kind) <- SourceType -> m (SourceType, SourceType)
kindOf SourceType
a
  (SourceType
b', SourceType
kind') <- SourceType -> m (SourceType, SourceType)
kindOf SourceType
b
  forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> SourceType -> m ()
unifyKinds' SourceType
kind SourceType
kind'
  Substitution
subst <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Substitution
checkSubstitution
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Substitution -> SourceType -> SourceType
substituteType Substitution
subst SourceType
kind
       , Substitution -> SourceType -> SourceType
substituteType Substitution
subst SourceType
a'
       , Substitution -> SourceType -> SourceType
substituteType Substitution
subst SourceType
b'
       )

-- | A successful interaction between an irreducible constraint and an inert
--  given constraint has two possible outcomes:
data Interaction
  = Simplified (SourceType, SourceType)
  -- ^ The interaction can yield a derived constraint,
  | Discharged
  -- ^ or we can learn the irreducible constraint is redundant and discharge it.

-- | Interact an irreducible constraint with an inert set of givens.
interact
  :: Environment
  -> (SourceType, SourceType)
  -> [(SourceType, SourceType, SourceType)]
  -> Maybe Interaction
interact :: Environment
-> (SourceType, SourceType)
-> [(SourceType, SourceType, SourceType)]
-> Maybe Interaction
interact Environment
env (SourceType, SourceType)
irred = [(SourceType, SourceType, SourceType)] -> Maybe Interaction
go where
  go :: [(SourceType, SourceType, SourceType)] -> Maybe Interaction
go [] = forall a. Maybe a
Nothing
  go ((SourceType, SourceType, SourceType)
inert : [(SourceType, SourceType, SourceType)]
_)
    | (SourceType, SourceType, SourceType)
-> (SourceType, SourceType) -> Bool
canDischarge (SourceType, SourceType, SourceType)
inert (SourceType, SourceType)
irred = forall a. a -> Maybe a
Just Interaction
Discharged
    | Just (SourceType, SourceType)
derived <- (SourceType, SourceType, SourceType)
-> (SourceType, SourceType) -> Maybe (SourceType, SourceType)
interactSameTyVar (SourceType, SourceType, SourceType)
inert (SourceType, SourceType)
irred = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ (SourceType, SourceType) -> Interaction
Simplified (SourceType, SourceType)
derived
    | Just (SourceType, SourceType)
derived <- Environment
-> (SourceType, SourceType, SourceType)
-> (SourceType, SourceType)
-> Maybe (SourceType, SourceType)
interactDiffTyVar Environment
env (SourceType, SourceType, SourceType)
inert (SourceType, SourceType)
irred = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ (SourceType, SourceType) -> Interaction
Simplified (SourceType, SourceType)
derived
  go ((SourceType, SourceType, SourceType)
_ : [(SourceType, SourceType, SourceType)]
inerts) = [(SourceType, SourceType, SourceType)] -> Maybe Interaction
go [(SourceType, SourceType, SourceType)]
inerts

-- | A given constraint of the form @Coercible a b@ can discharge constraints
-- of the form @Coercible a b@ and @Coercible b a@.
canDischarge
  :: (SourceType, SourceType, SourceType)
  -> (SourceType, SourceType)
  -> Bool
canDischarge :: (SourceType, SourceType, SourceType)
-> (SourceType, SourceType) -> Bool
canDischarge (SourceType
_, SourceType
a, SourceType
b) (SourceType, SourceType)
constraint =
  (SourceType
a, SourceType
b) forall a. Eq a => a -> a -> Bool
== (SourceType, SourceType)
constraint Bool -> Bool -> Bool
|| (SourceType
b, SourceType
a) forall a. Eq a => a -> a -> Bool
== (SourceType, SourceType)
constraint

-- | Two canonical constraints of the form @Coercible tv ty1@ and
-- @Coercible tv ty2@ can interact together and yield a new constraint
-- @Coercible ty1 ty2@. Canonicality matters to avoid loops.
--
-- For instance the declarations:
--
-- @
-- data D a = D a
-- newtype N a = N (D (N a))
--
-- example :: forall a. Coercible a (D a) => a -> N a
-- example = coerce
-- @
--
-- yield a non canonical wanted @Coercible a (N a)@ that we can unwrap on the
-- right to yield @Coercible a (D (N a))@. Would it interact with the non
-- canonical given @Coercible a (D a)@ it would give @Coercible (D a) (D (N a))@,
-- then decompose back to @Coercible a (N a)@.
interactSameTyVar
  :: (SourceType, SourceType, SourceType)
  -> (SourceType, SourceType)
  -> Maybe (SourceType, SourceType)
interactSameTyVar :: (SourceType, SourceType, SourceType)
-> (SourceType, SourceType) -> Maybe (SourceType, SourceType)
interactSameTyVar (SourceType
_, SourceType
tv1, SourceType
ty1) (SourceType
tv2, SourceType
ty2)
  | SourceType
tv1 forall a. Eq a => a -> a -> Bool
== SourceType
tv2 Bool -> Bool -> Bool
&& (SourceType, SourceType) -> Bool
isCanonicalTyVarEq (SourceType
tv1, SourceType
ty1) Bool -> Bool -> Bool
&& (SourceType, SourceType) -> Bool
isCanonicalTyVarEq (SourceType
tv2, SourceType
ty2)
  = forall a. a -> Maybe a
Just (SourceType
ty1, SourceType
ty2)
  | Bool
otherwise = forall a. Maybe a
Nothing

-- | Two canonical constraints of the form @Coercible tv1 ty1@ and
-- @Coercible tv2 ty2@ can interact together and yield a new constraint
-- @Coercible tv2 ty2[ty1/tv1]@. Once again, canonicality matters to avoid loops.
--
-- For instance the declarations:
--
-- @
-- data D a = D a
--
-- example :: forall a b. Coercible b (D b) => a -> b
-- example = coerce
-- @
--
-- yield an irreducible canonical wanted @Coercible a b@. Would it interact with
-- the non canonical given @Coercible b (D b)@ it would give @Coercible a (D b)@,
-- which would keep interacting indefinitely with the given.
interactDiffTyVar
  :: Environment
  -> (SourceType, SourceType, SourceType)
  -> (SourceType, SourceType)
  -> Maybe (SourceType, SourceType)
interactDiffTyVar :: Environment
-> (SourceType, SourceType, SourceType)
-> (SourceType, SourceType)
-> Maybe (SourceType, SourceType)
interactDiffTyVar Environment
env (SourceType
_, SourceType
tv1, SourceType
ty1) (SourceType
tv2, SourceType
ty2)
  | SourceType
tv1 forall a. Eq a => a -> a -> Bool
/= SourceType
tv2 Bool -> Bool -> Bool
&& (SourceType, SourceType) -> Bool
isCanonicalTyVarEq (SourceType
tv2, SourceType
ty2)
  , (SourceType
ty2', Any Bool
True) <- forall w a. Writer w a -> (a, w)
runWriter forall a b. (a -> b) -> a -> b
$ Environment
-> (SourceType, SourceType) -> SourceType -> Writer Any SourceType
rewrite Environment
env (SourceType
tv1, SourceType
ty1) SourceType
ty2
  = forall a. a -> Maybe a
Just (SourceType
tv2, SourceType
ty2')
  | Bool
otherwise = forall a. Maybe a
Nothing

-- | A canonical constraint of the form @Coercible tv1 ty1@ can rewrite the
-- right hand side of an irreducible constraint of the form @Coercible tv2 ty2@
-- by substituting @ty1@ for every occurence of @tv1@ at representational and
-- phantom role in @ty2@. Nominal occurences are left untouched.
rewrite :: Environment -> (SourceType, SourceType) -> SourceType -> Writer Any SourceType
rewrite :: Environment
-> (SourceType, SourceType) -> SourceType -> Writer Any SourceType
rewrite Environment
env (Skolem SourceAnn
_ Text
_ Maybe SourceType
_ Int
s1 SkolemScope
_, SourceType
ty1) | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Int -> SourceType -> Bool
occurs Int
s1 SourceType
ty1 = SourceType -> Writer Any SourceType
go where
  go :: SourceType -> Writer Any SourceType
go (Skolem SourceAnn
_ Text
_ Maybe SourceType
_ Int
s2 SkolemScope
_) | Int
s1 forall a. Eq a => a -> a -> Bool
== Int
s2 = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Bool -> Any
Any Bool
True) forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceType
ty1
  go SourceType
ty2 | (Skolem{}, [SourceType]
_, [SourceType]
xs) <- forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes SourceType
ty2, Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SourceType]
xs =
    forall (m :: * -> *).
Applicative m =>
(SourceType -> m SourceType) -> SourceType -> m SourceType
rewriteTyVarApp SourceType -> Writer Any SourceType
go SourceType
ty2
         | (TypeConstructor SourceAnn
_ Qualified (ProperName 'TypeName)
tyName, [SourceType]
_, [SourceType]
_) <- forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes SourceType
ty2 = do
    forall (m :: * -> *).
Applicative m =>
(SourceType -> m SourceType)
-> [Role] -> SourceType -> m SourceType
rewriteTyConApp SourceType -> Writer Any SourceType
go (Environment -> Qualified (ProperName 'TypeName) -> [Role]
lookupRoles Environment
env Qualified (ProperName 'TypeName)
tyName) SourceType
ty2
  go (KindApp SourceAnn
sa SourceType
ty SourceType
k) = forall a. a -> Type a -> Type a -> Type a
KindApp SourceAnn
sa forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceType -> Writer Any SourceType
go SourceType
ty forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
k
  go (ForAll SourceAnn
sa Text
tv Maybe SourceType
k SourceType
ty Maybe SkolemScope
scope) = forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll SourceAnn
sa Text
tv Maybe SourceType
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceType -> Writer Any SourceType
go SourceType
ty forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe SkolemScope
scope
  go (ConstrainedType SourceAnn
sa Constraint{[SourceType]
Maybe ConstraintData
SourceAnn
Qualified (ProperName 'ClassName)
constraintData :: forall a. Constraint a -> Maybe ConstraintData
constraintArgs :: forall a. Constraint a -> [Type a]
constraintKindArgs :: forall a. Constraint a -> [Type a]
constraintClass :: forall a. Constraint a -> Qualified (ProperName 'ClassName)
constraintAnn :: forall a. Constraint a -> a
constraintData :: Maybe ConstraintData
constraintArgs :: [SourceType]
constraintKindArgs :: [SourceType]
constraintClass :: Qualified (ProperName 'ClassName)
constraintAnn :: SourceAnn
..} SourceType
ty) | Int
s1 forall a. Ord a => a -> Set a -> Bool
`S.notMember` forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap SourceType -> Set Int
skolems [SourceType]
constraintArgs =
    forall a. a -> Constraint a -> Type a -> Type a
ConstrainedType SourceAnn
sa Constraint{[SourceType]
Maybe ConstraintData
SourceAnn
Qualified (ProperName 'ClassName)
constraintData :: Maybe ConstraintData
constraintArgs :: [SourceType]
constraintKindArgs :: [SourceType]
constraintClass :: Qualified (ProperName 'ClassName)
constraintAnn :: SourceAnn
constraintData :: Maybe ConstraintData
constraintArgs :: [SourceType]
constraintKindArgs :: [SourceType]
constraintClass :: Qualified (ProperName 'ClassName)
constraintAnn :: SourceAnn
..} forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceType -> Writer Any SourceType
go SourceType
ty
  go (RCons SourceAnn
sa Label
label SourceType
ty SourceType
rest) = forall a. a -> Label -> Type a -> Type a -> Type a
RCons SourceAnn
sa Label
label forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceType -> Writer Any SourceType
go SourceType
ty forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SourceType -> Writer Any SourceType
go SourceType
rest
  go (KindedType SourceAnn
sa SourceType
ty SourceType
k) = forall a. a -> Type a -> Type a -> Type a
KindedType SourceAnn
sa forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceType -> Writer Any SourceType
go SourceType
ty forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
k
  go SourceType
ty2 = forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
ty2
rewrite Environment
_ (SourceType, SourceType)
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Rewrite the head of a type application of the form @tv a_0 .. a_n@.
rewriteTyVarApp
  :: Applicative m
  => (SourceType -> m SourceType)
  -> SourceType
  -> m SourceType
rewriteTyVarApp :: forall (m :: * -> *).
Applicative m =>
(SourceType -> m SourceType) -> SourceType -> m SourceType
rewriteTyVarApp SourceType -> m SourceType
f = SourceType -> m SourceType
go where
  go :: SourceType -> m SourceType
go (TypeApp SourceAnn
sa SourceType
lhs SourceType
rhs) =
    forall a. a -> Type a -> Type a -> Type a
TypeApp SourceAnn
sa forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceType -> m SourceType
go SourceType
lhs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
rhs
  go (KindApp SourceAnn
sa SourceType
ty SourceType
k) =
    forall a. a -> Type a -> Type a -> Type a
KindApp SourceAnn
sa forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceType -> m SourceType
go SourceType
ty forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
k
  go SourceType
ty = SourceType -> m SourceType
f SourceType
ty

-- | Rewrite the representational and phantom arguments of a type application
-- of the form @D a_0 .. a_n@.
rewriteTyConApp
  :: Applicative m
  => (SourceType -> m SourceType)
  -> [Role]
  -> SourceType
  -> m SourceType
rewriteTyConApp :: forall (m :: * -> *).
Applicative m =>
(SourceType -> m SourceType)
-> [Role] -> SourceType -> m SourceType
rewriteTyConApp SourceType -> m SourceType
f = [Role] -> SourceType -> m SourceType
go where
  go :: [Role] -> SourceType -> m SourceType
go (Role
role : [Role]
roles) (TypeApp SourceAnn
sa SourceType
lhs SourceType
rhs) =
    forall a. a -> Type a -> Type a -> Type a
TypeApp SourceAnn
sa forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Role] -> SourceType -> m SourceType
go [Role]
roles SourceType
lhs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> case Role
role of
      Role
Nominal -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
rhs
      Role
_ -> SourceType -> m SourceType
f SourceType
rhs
  go [Role]
roles (KindApp SourceAnn
sa SourceType
ty SourceType
k) =
    forall a. a -> Type a -> Type a -> Type a
KindApp SourceAnn
sa forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Role] -> SourceType -> m SourceType
go [Role]
roles SourceType
ty forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
k
  go [Role]
_ SourceType
ty = forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
ty

canRewrite :: Environment -> (SourceType, SourceType) -> SourceType -> Bool
canRewrite :: Environment -> (SourceType, SourceType) -> SourceType -> Bool
canRewrite Environment
env (SourceType, SourceType)
irred = Any -> Bool
getAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w a. Writer w a -> w
execWriter forall b c a. (b -> c) -> (a -> b) -> a -> c
. Environment
-> (SourceType, SourceType) -> SourceType -> Writer Any SourceType
rewrite Environment
env (SourceType, SourceType)
irred

-- | An irreducible given constraint must kick out of the inert set any
-- constraint it can rewrite when it becomes inert, otherwise solving would be
-- sensitive to the order of constraints. Wanteds cannot rewrite other wanteds
-- so this applies only to givens.
--
-- For instance the declaration:
--
-- @
-- example :: forall f g a b. Coercible a (f b) => Coercible f g => Proxy f -> a -> g b
-- example _ = coerce
-- @
--
-- yields the irreducible givens @Coercible a (f b)@ and @Coercible f g@. Would
-- we not kick out the former when adding the latter to the inert set we would
-- not be able to rewrite it to @Coercible a (g b)@ and discharge the wanted,
-- but inverting the givens would work.
kicksOut
  :: Environment
  -> (SourceType, SourceType)
  -> (SourceType, SourceType, SourceType)
  -> Either (SourceType, SourceType) (SourceType, SourceType, SourceType)
kicksOut :: Environment
-> (SourceType, SourceType)
-> (SourceType, SourceType, SourceType)
-> Either
     (SourceType, SourceType) (SourceType, SourceType, SourceType)
kicksOut Environment
env (SourceType, SourceType)
irred (SourceType
_, SourceType
tv2, SourceType
ty2)
  | (SourceType, SourceType) -> Bool
isCanonicalTyVarEq (SourceType
tv2, SourceType
ty2) Bool -> Bool -> Bool
&& Environment -> (SourceType, SourceType) -> SourceType -> Bool
canRewrite Environment
env (SourceType, SourceType)
irred SourceType
ty2
  = forall a b. a -> Either a b
Left (SourceType
tv2, SourceType
ty2)
kicksOut Environment
_ (SourceType, SourceType)
_ (SourceType, SourceType, SourceType)
inert = forall a b. b -> Either a b
Right (SourceType, SourceType, SourceType)
inert

-- | A constraint of the form @Coercible tv ty@ is canonical when @tv@ does not
-- occur in @ty@. Non canonical constraints do not interact to prevent loops.
isCanonicalTyVarEq :: (SourceType, SourceType) -> Bool
isCanonicalTyVarEq :: (SourceType, SourceType) -> Bool
isCanonicalTyVarEq (Skolem SourceAnn
_ Text
_ Maybe SourceType
_ Int
s SkolemScope
_, SourceType
ty) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Int -> SourceType -> Bool
occurs Int
s SourceType
ty
isCanonicalTyVarEq (SourceType, SourceType)
_ = Bool
False

occurs :: Int -> SourceType -> Bool
occurs :: Int -> SourceType -> Bool
occurs Int
s1 = forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes Bool -> Bool -> Bool
(||) SourceType -> Bool
go where
  go :: SourceType -> Bool
go (Skolem SourceAnn
_ Text
_ Maybe SourceType
_ Int
s2 SkolemScope
_) | Int
s1 forall a. Eq a => a -> a -> Bool
== Int
s2 = Bool
True
  go SourceType
_ = Bool
False

skolems :: SourceType -> S.Set Int
skolems :: SourceType -> Set Int
skolems = forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes forall a. Semigroup a => a -> a -> a
(<>) forall {a}. Type a -> Set Int
go where
  go :: Type a -> Set Int
go (Skolem a
_ Text
_ Maybe (Type a)
_ Int
s SkolemScope
_) = forall a. a -> Set a
S.singleton Int
s
  go Type a
_ = forall a. Monoid a => a
mempty

-- | A successful canonicalization result has two possible outcomes:
data Canonicalized
  = Canonicalized (S.Set (SourceType, SourceType))
  -- ^ Canonicalization can yield a set of derived constraints,
  | Irreducible
  -- ^ or we can learn the constraint is irreducible. Irreducibility is not
  -- necessarily an error, we may make further progress by interacting with
  -- inerts.

-- | Canonicalization takes a wanted constraint and try to reduce it to a set of
-- simpler constraints whose satisfaction will imply the goal.
canon
  :: MonadError MultipleErrors m
  => MonadWriter [ErrorMessageHint] m
  => MonadState CheckState m
  => Environment
  -> Maybe [(SourceType, SourceType, SourceType)]
  -> SourceType
  -> SourceType
  -> SourceType
  -> m Canonicalized
canon :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadWriter [ErrorMessageHint] m,
 MonadState CheckState m) =>
Environment
-> Maybe [(SourceType, SourceType, SourceType)]
-> SourceType
-> SourceType
-> SourceType
-> m Canonicalized
canon Environment
env Maybe [(SourceType, SourceType, SourceType)]
givens SourceType
k SourceType
a SourceType
b =
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> SourceType -> MultipleErrors
insoluble SourceType
k SourceType
a SourceType
b) forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *).
Monad m =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonRefl SourceType
a SourceType
b
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Environment -> SourceType -> SourceType -> MaybeT m Canonicalized
canonUnsaturatedHigherKindedType Environment
env SourceType
a SourceType
b
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonRow SourceType
a SourceType
b
    -- We unwrap newtypes before trying the decomposition rules because it let
    -- us solve more constraints.
    --
    -- For instance the declarations:
    --
    -- @
    -- newtype N f a = N (f a)
    --
    -- example :: forall a b. Coercible a b => N Maybe a -> N Maybe b
    -- example = coerce
    -- @
    --
    -- yield the wanted @Coercible (N Maybe a) (N Maybe b)@ which we cannot
    -- decompose because the second parameter of @N@ is nominal. On the other
    -- hand, unwraping on both sides yields @Coercible (Maybe a) (Maybe b)@
    -- which we can then decompose to @Coercible a b@ and discharge with the
    -- given.
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *).
(MonadState CheckState m, MonadWriter [ErrorMessageHint] m) =>
Environment -> SourceType -> SourceType -> MaybeT m Canonicalized
canonNewtypeLeft Environment
env SourceType
a SourceType
b
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *).
(MonadState CheckState m, MonadWriter [ErrorMessageHint] m) =>
Environment -> SourceType -> SourceType -> MaybeT m Canonicalized
canonNewtypeRight Environment
env SourceType
a SourceType
b
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Environment -> SourceType -> SourceType -> MaybeT m Canonicalized
canonDecomposition Environment
env SourceType
a SourceType
b
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Environment
-> SourceType -> SourceType -> SourceType -> MaybeT m Canonicalized
canonDecompositionFailure Environment
env SourceType
k SourceType
a SourceType
b
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Environment
-> Maybe [(SourceType, SourceType, SourceType)]
-> SourceType
-> SourceType
-> MaybeT m Canonicalized
canonNewtypeDecomposition Environment
env Maybe [(SourceType, SourceType, SourceType)]
givens SourceType
a SourceType
b
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *).
Monad m =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonNewtypeDecompositionFailure SourceType
a SourceType
b
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *).
Monad m =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonTypeVars SourceType
a SourceType
b
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *).
Monad m =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonTypeVarLeft SourceType
a SourceType
b
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *).
Monad m =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonTypeVarRight SourceType
a SourceType
b
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *).
Monad m =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonApplicationLeft SourceType
a SourceType
b
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *).
Monad m =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonApplicationRight SourceType
a SourceType
b

insoluble
  :: SourceType
  -> SourceType
  -> SourceType
  -> MultipleErrors
insoluble :: SourceType -> SourceType -> SourceType -> MultipleErrors
insoluble SourceType
k SourceType
a SourceType
b =
  -- We can erase kind applications when determining whether to show the
  -- "Consider adding a type annotation" hint, because annotating kinds to
  -- instantiate unknowns in Coercible constraints should never resolve
  -- NoInstanceFound errors.
  SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ Constraint SourceAnn
-> [Qualified (Either SourceType Ident)]
-> Bool
-> SimpleErrorMessage
NoInstanceFound (Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> Maybe ConstraintData
-> Constraint SourceAnn
srcConstraint Qualified (ProperName 'ClassName)
Prim.Coercible [SourceType
k] [SourceType
a, SourceType
b] forall a. Maybe a
Nothing) [] (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. Type a -> Bool
containsUnknowns [SourceType
a, SourceType
b])

-- | Constraints of the form @Coercible a b@ can be solved if the two arguments
-- are the same. Since we currently don't support higher-rank arguments in
-- instance heads, term equality is a sufficient notion of "the same".
canonRefl
  :: Monad m
  => SourceType
  -> SourceType
  -> MaybeT m Canonicalized
canonRefl :: forall (m :: * -> *).
Monad m =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonRefl SourceType
a SourceType
b =
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard (SourceType
a forall a. Eq a => a -> a -> Bool
== SourceType
b) forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Set (SourceType, SourceType) -> Canonicalized
Canonicalized forall a. Monoid a => a
mempty

-- | Constraints of the form @Coercible (T1 a_0 .. a_n) (T2 b_0 .. b_n)@, where
-- both arguments have kind @k1 -> k2@, yield a constraint
-- @Coercible (T1 a_0 .. a_n c_0 .. c_m) (T2 b_0 .. b_n c_0 .. c_m)@, where both
-- arguments are fully saturated with the same unknowns and have kind @Type@.
canonUnsaturatedHigherKindedType
  :: MonadError MultipleErrors m
  => MonadState CheckState m
  => Environment
  -> SourceType
  -> SourceType
  -> MaybeT m Canonicalized
canonUnsaturatedHigherKindedType :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Environment -> SourceType -> SourceType -> MaybeT m Canonicalized
canonUnsaturatedHigherKindedType Environment
env SourceType
a SourceType
b
  | (TypeConstructor SourceAnn
_ Qualified (ProperName 'TypeName)
aTyName, [SourceType]
akapps, [SourceType]
axs) <- forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes SourceType
a
  , (SourceType
ak, TypeKind
_) <- forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
internalError String
"canonUnsaturatedHigherKindedType: type lookup failed") forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'TypeName)
aTyName (Environment
-> Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
types Environment
env)
  , ([SourceType]
aks, SourceType
_) <- forall a. Type a -> ([Type a], Type a)
unapplyKinds SourceType
ak
  , forall (t :: * -> *) a. Foldable t => t a -> Int
length [SourceType]
axs forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length [SourceType]
aks = do
      SourceType
ak' <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ do
        let ([(SourceAnn, (Text, SourceType))]
kvs, SourceType
ak') = forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
internalError String
"canonUnsaturatedHigherKindedType: unkinded forall binder") forall a b. (a -> b) -> a -> b
$ forall a. Type a -> Maybe ([(a, (Text, Type a))], Type a)
completeBinderList SourceType
ak
            instantiatedKinds :: [(Text, SourceType)]
instantiatedKinds = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(SourceAnn
_, (Text
kv, SourceType
_)) SourceType
k -> (Text
kv, SourceType
k)) [(SourceAnn, (Text, SourceType))]
kvs [SourceType]
akapps
        [(Text, SourceType)]
unknownKinds <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\((SourceSpan
ss, [Comment]
_), (Text
kv, SourceType
k)) -> (Text
kv,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadState CheckState m =>
SourceSpan -> SourceType -> m SourceType
freshKindWithKind SourceSpan
ss SourceType
k) forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length [SourceType]
akapps) [(SourceAnn, (Text, SourceType))]
kvs
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. [(Text, Type a)] -> Type a -> Type a
replaceAllTypeVars ([(Text, SourceType)]
instantiatedKinds forall a. Semigroup a => a -> a -> a
<> [(Text, SourceType)]
unknownKinds) SourceType
ak'
      let ([SourceType]
aks', SourceType
_) = forall a. Type a -> ([Type a], Type a)
unapplyKinds SourceType
ak'
      [SourceType]
tys <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length [SourceType]
axs) [SourceType]
aks'
      let a' :: SourceType
a' = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' SourceType -> SourceType -> SourceType
srcTypeApp SourceType
a [SourceType]
tys
          b' :: SourceType
b' = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' SourceType -> SourceType -> SourceType
srcTypeApp SourceType
b [SourceType]
tys
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (SourceType, SourceType) -> Canonicalized
Canonicalized forall a b. (a -> b) -> a -> b
$ forall a. a -> Set a
S.singleton (SourceType
a', SourceType
b')
  | Bool
otherwise = forall (f :: * -> *) a. Alternative f => f a
empty

-- | Constraints of the form
-- @Coercible ( label_0 :: a_0, .. label_n :: a_n | r ) ( label_0 :: b_0, .. label_n :: b_n | s )@
-- yield a constraint @Coercible r s@ and constraints on the types for each
-- label in both rows. Labels exclusive to one row yield a failure.
canonRow
  :: MonadError MultipleErrors m
  => MonadState CheckState m
  => SourceType
  -> SourceType
  -> MaybeT m Canonicalized
canonRow :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonRow SourceType
a SourceType
b
  | RCons{} <- SourceType
a =
      case forall a r.
(Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith (,) SourceType
a SourceType
b of
        -- We throw early when a bare unknown remains on either side after
        -- aligning the rows because we don't know how to canonicalize them yet
        -- and the unification error thrown when the rows are misaligned should
        -- not mention unknowns.
        ([(SourceType, SourceType)]
_, (([], u :: SourceType
u@TUnknown{}), ([RowListItem SourceAnn], SourceType)
rl2)) -> do
          SourceType
k <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> m SourceType
elaborateKind SourceType
u
          forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> SourceType -> MultipleErrors
insoluble SourceType
k SourceType
u (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn], SourceType)
rl2)
        ([(SourceType, SourceType)]
_, (([RowListItem SourceAnn], SourceType)
rl1, ([], u :: SourceType
u@TUnknown{}))) -> do
          SourceType
k <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
 HasCallStack) =>
SourceType -> m SourceType
elaborateKind SourceType
u
          forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> SourceType -> MultipleErrors
insoluble SourceType
k (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn], SourceType)
rl1) SourceType
u
        ([(SourceType, SourceType)]
deriveds, (([], SourceType
tail1), ([], SourceType
tail2))) -> do
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (SourceType, SourceType) -> Canonicalized
Canonicalized forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ (SourceType
tail1, SourceType
tail2) forall a. a -> [a] -> [a]
: [(SourceType, SourceType)]
deriveds
        ([(SourceType, SourceType)]
_, (([RowListItem SourceAnn], SourceType)
rl1, ([RowListItem SourceAnn], SourceType)
rl2)) ->
          forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> SimpleErrorMessage
TypesDoNotUnify (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn], SourceType)
rl1) (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn], SourceType)
rl2)
  | Bool
otherwise = forall (f :: * -> *) a. Alternative f => f a
empty

-- | Unwraping a newtype can fails in two ways:
data UnwrapNewtypeError
  = CannotUnwrapInfiniteNewtypeChain
  -- ^ The newtype might wrap an infinite newtype chain. We may think that this
  -- is already handled by the solver depth check, but failing to unwrap
  -- infinite chains of newtypes let us try other rules.
  --
  -- For instance the declarations:
  --
  -- @
  -- newtype N a = N (N a)
  -- type role N representational
  --
  -- example :: forall a b. Coercible a b => N a -> N b
  -- example = coerce
  -- @
  --
  -- yield a wanted @Coercible (N a) (N b)@ that we can decompose to
  -- @Coercible a b@ then discharge with the given if the newtype
  -- unwraping rules do not apply.
  | CannotUnwrapConstructor
  -- ^ The constructor may not be in scope or may not belong to a newtype.

-- | Unwraps a newtype and yields its underlying type with the newtype arguments
-- substituted in (e.g. @N[D/a] = D@ given @newtype N a = N a@ and @data D = D@).
unwrapNewtype
  :: MonadState CheckState m
  => MonadWriter [ErrorMessageHint] m
  => Environment
  -> SourceType
  -> m (Either UnwrapNewtypeError SourceType)
unwrapNewtype :: forall (m :: * -> *).
(MonadState CheckState m, MonadWriter [ErrorMessageHint] m) =>
Environment
-> SourceType -> m (Either UnwrapNewtypeError SourceType)
unwrapNewtype Environment
env = Int -> SourceType -> m (Either UnwrapNewtypeError SourceType)
go (Int
0 :: Int) where
  go :: Int -> SourceType -> m (Either UnwrapNewtypeError SourceType)
go Int
n SourceType
ty = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ do
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n forall a. Ord a => a -> a -> Bool
> Int
1000) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError UnwrapNewtypeError
CannotUnwrapInfiniteNewtypeChain
    (Maybe ModuleName
currentModuleName, [(SourceAnn, ModuleName, ImportDeclarationType, Maybe ModuleName,
  Map
    (ProperName 'TypeName)
    ([ProperName 'ConstructorName], ExportSource))]
currentModuleImports) <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ CheckState -> Maybe ModuleName
checkCurrentModule forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& CheckState
-> [(SourceAnn, ModuleName, ImportDeclarationType,
     Maybe ModuleName,
     Map
       (ProperName 'TypeName)
       ([ProperName 'ConstructorName], ExportSource))]
checkCurrentModuleImports
    case forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes SourceType
ty of
      (TypeConstructor SourceAnn
_ Qualified (ProperName 'TypeName)
newtypeName, [SourceType]
ks, [SourceType]
xs)
        | Just (Bool
inScope, Maybe ModuleName
fromModuleName, [Text]
tvs, Qualified (ProperName 'ConstructorName)
newtypeCtorName, SourceType
wrappedTy) <-
            Environment
-> Maybe ModuleName
-> [(SourceAnn, ModuleName, ImportDeclarationType,
     Maybe ModuleName,
     Map
       (ProperName 'TypeName)
       ([ProperName 'ConstructorName], ExportSource))]
-> Qualified (ProperName 'TypeName)
-> [SourceType]
-> Maybe
     (Bool, Maybe ModuleName, [Text],
      Qualified (ProperName 'ConstructorName), SourceType)
lookupNewtypeConstructorInScope Environment
env Maybe ModuleName
currentModuleName [(SourceAnn, ModuleName, ImportDeclarationType, Maybe ModuleName,
  Map
    (ProperName 'TypeName)
    ([ProperName 'ConstructorName], ExportSource))]
currentModuleImports Qualified (ProperName 'TypeName)
newtypeName [SourceType]
ks
        -- We refuse to unwrap newtypes over polytypes because we don't know how
        -- to canonicalize them yet and we'd rather try to make progress with
        -- another rule.
        , forall a. Type a -> Bool
isMonoType SourceType
wrappedTy -> do
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
inScope forall a b. (a -> b) -> a -> b
$ do
              forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Qualified (ProperName 'ConstructorName) -> ErrorMessageHint
MissingConstructorImportForCoercible Qualified (ProperName 'ConstructorName)
newtypeCtorName]
              forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError UnwrapNewtypeError
CannotUnwrapConstructor
            forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ Maybe ModuleName
fromModuleName forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall {m :: * -> *}.
MonadState CheckState m =>
ModuleName -> Qualified (ProperName 'ConstructorName) -> m ()
addConstructorImportForCoercible Qualified (ProperName 'ConstructorName)
newtypeCtorName
            let wrappedTySub :: SourceType
wrappedTySub = forall a. [(Text, Type a)] -> Type a -> Type a
replaceAllTypeVars (forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
tvs [SourceType]
xs) SourceType
wrappedTy
            forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (Int -> SourceType -> m (Either UnwrapNewtypeError SourceType)
go (Int
n forall a. Num a => a -> a -> a
+ Int
1) SourceType
wrappedTySub) forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
              UnwrapNewtypeError
CannotUnwrapInfiniteNewtypeChain -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError UnwrapNewtypeError
CannotUnwrapInfiniteNewtypeChain
              UnwrapNewtypeError
CannotUnwrapConstructor -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
wrappedTySub
      (SourceType, [SourceType], [SourceType])
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError UnwrapNewtypeError
CannotUnwrapConstructor
  addConstructorImportForCoercible :: ModuleName -> Qualified (ProperName 'ConstructorName) -> m ()
addConstructorImportForCoercible ModuleName
fromModuleName Qualified (ProperName 'ConstructorName)
newtypeCtorName = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CheckState
st ->
    CheckState
st { checkConstructorImportsForCoercible :: Set (ModuleName, Qualified (ProperName 'ConstructorName))
checkConstructorImportsForCoercible = forall a. Ord a => a -> Set a -> Set a
S.insert (ModuleName
fromModuleName, Qualified (ProperName 'ConstructorName)
newtypeCtorName) forall a b. (a -> b) -> a -> b
$ CheckState
-> Set (ModuleName, Qualified (ProperName 'ConstructorName))
checkConstructorImportsForCoercible CheckState
st }

-- | Looks up a given name and, if it names a newtype, returns the names of the
-- type's parameters, the type the newtype wraps and the names of the type's
-- fields.
lookupNewtypeConstructor
  :: Environment
  -> Qualified (ProperName 'TypeName)
  -> [SourceType]
  -> Maybe ([Text], ProperName 'ConstructorName, SourceType)
lookupNewtypeConstructor :: Environment
-> Qualified (ProperName 'TypeName)
-> [SourceType]
-> Maybe ([Text], ProperName 'ConstructorName, SourceType)
lookupNewtypeConstructor Environment
env Qualified (ProperName 'TypeName)
qualifiedNewtypeName [SourceType]
ks = do
  (SourceType
newtyk, DataType DataDeclType
Newtype [(Text, Maybe SourceType, Role)]
tvs [(ProperName 'ConstructorName
ctorName, [SourceType
wrappedTy])]) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'TypeName)
qualifiedNewtypeName (Environment
-> Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
types Environment
env)
  let ([(SourceAnn, (Text, SourceType))]
kvs, SourceType
_) = forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
internalError String
"lookupNewtypeConstructor: unkinded forall binder") forall a b. (a -> b) -> a -> b
$ forall a. Type a -> Maybe ([(a, (Text, Type a))], Type a)
completeBinderList SourceType
newtyk
      instantiatedKinds :: [(Text, SourceType)]
instantiatedKinds = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(SourceAnn
_, (Text
kv, SourceType
_)) SourceType
k -> (Text
kv, SourceType
k)) [(SourceAnn, (Text, SourceType))]
kvs [SourceType]
ks
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a -> b) -> [a] -> [b]
map (\(Text
name, Maybe SourceType
_, Role
_) -> Text
name) [(Text, Maybe SourceType, Role)]
tvs, ProperName 'ConstructorName
ctorName, forall a. [(Text, Type a)] -> Type a -> Type a
replaceAllTypeVars [(Text, SourceType)]
instantiatedKinds SourceType
wrappedTy)

-- | Behaves like 'lookupNewtypeConstructor' but also returns whether the
-- newtype constructor is in scope and the module from which it is imported, or
-- 'Nothing' if it is defined in the current module.
lookupNewtypeConstructorInScope
  :: Environment
  -> Maybe ModuleName
  -> [ ( SourceAnn
       , ModuleName
       , ImportDeclarationType
       , Maybe ModuleName
       , M.Map (ProperName 'TypeName) ([ProperName 'ConstructorName], ExportSource)
       )
     ]
  -> Qualified (ProperName 'TypeName)
  -> [SourceType]
  -> Maybe (Bool, Maybe ModuleName, [Text], Qualified (ProperName 'ConstructorName), SourceType)
lookupNewtypeConstructorInScope :: Environment
-> Maybe ModuleName
-> [(SourceAnn, ModuleName, ImportDeclarationType,
     Maybe ModuleName,
     Map
       (ProperName 'TypeName)
       ([ProperName 'ConstructorName], ExportSource))]
-> Qualified (ProperName 'TypeName)
-> [SourceType]
-> Maybe
     (Bool, Maybe ModuleName, [Text],
      Qualified (ProperName 'ConstructorName), SourceType)
lookupNewtypeConstructorInScope Environment
env Maybe ModuleName
currentModuleName [(SourceAnn, ModuleName, ImportDeclarationType, Maybe ModuleName,
  Map
    (ProperName 'TypeName)
    ([ProperName 'ConstructorName], ExportSource))]
currentModuleImports qualifiedNewtypeName :: Qualified (ProperName 'TypeName)
qualifiedNewtypeName@(Qualified QualifiedBy
newtypeModuleName ProperName 'TypeName
newtypeName) [SourceType]
ks = do
  let fromModule :: Maybe
  (SourceAnn, ModuleName, ImportDeclarationType, Maybe ModuleName,
   Map
     (ProperName 'TypeName)
     ([ProperName 'ConstructorName], ExportSource))
fromModule = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (SourceAnn, ModuleName, ImportDeclarationType, Maybe ModuleName,
 Map
   (ProperName 'TypeName)
   ([ProperName 'ConstructorName], ExportSource))
-> Bool
isNewtypeCtorImported [(SourceAnn, ModuleName, ImportDeclarationType, Maybe ModuleName,
  Map
    (ProperName 'TypeName)
    ([ProperName 'ConstructorName], ExportSource))]
currentModuleImports
      fromModuleName :: Maybe ModuleName
fromModuleName = (\(SourceAnn
_, ModuleName
n, ImportDeclarationType
_, Maybe ModuleName
_, Map
  (ProperName 'TypeName)
  ([ProperName 'ConstructorName], ExportSource)
_) -> ModuleName
n) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe
  (SourceAnn, ModuleName, ImportDeclarationType, Maybe ModuleName,
   Map
     (ProperName 'TypeName)
     ([ProperName 'ConstructorName], ExportSource))
fromModule
      asModuleName :: Maybe ModuleName
asModuleName = (\(SourceAnn
_, ModuleName
_, ImportDeclarationType
_, Maybe ModuleName
n, Map
  (ProperName 'TypeName)
  ([ProperName 'ConstructorName], ExportSource)
_) -> Maybe ModuleName
n) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe
  (SourceAnn, ModuleName, ImportDeclarationType, Maybe ModuleName,
   Map
     (ProperName 'TypeName)
     ([ProperName 'ConstructorName], ExportSource))
fromModule
      isDefinedInCurrentModule :: Bool
isDefinedInCurrentModule = QualifiedBy -> Maybe ModuleName
toMaybeModuleName QualifiedBy
newtypeModuleName forall a. Eq a => a -> a -> Bool
== Maybe ModuleName
currentModuleName
      isImported :: Bool
isImported = forall a. Maybe a -> Bool
isJust Maybe
  (SourceAnn, ModuleName, ImportDeclarationType, Maybe ModuleName,
   Map
     (ProperName 'TypeName)
     ([ProperName 'ConstructorName], ExportSource))
fromModule
      inScope :: Bool
inScope = Bool
isDefinedInCurrentModule Bool -> Bool -> Bool
|| Bool
isImported
  ([Text]
tvs, ProperName 'ConstructorName
ctorName, SourceType
wrappedTy) <- Environment
-> Qualified (ProperName 'TypeName)
-> [SourceType]
-> Maybe ([Text], ProperName 'ConstructorName, SourceType)
lookupNewtypeConstructor Environment
env Qualified (ProperName 'TypeName)
qualifiedNewtypeName [SourceType]
ks
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
inScope, Maybe ModuleName
fromModuleName, [Text]
tvs, forall a. QualifiedBy -> a -> Qualified a
Qualified (Maybe ModuleName -> QualifiedBy
byMaybeModuleName Maybe ModuleName
asModuleName) ProperName 'ConstructorName
ctorName, SourceType
wrappedTy)
  where
  isNewtypeCtorImported :: (SourceAnn, ModuleName, ImportDeclarationType, Maybe ModuleName,
 Map
   (ProperName 'TypeName)
   ([ProperName 'ConstructorName], ExportSource))
-> Bool
isNewtypeCtorImported (SourceAnn
_, ModuleName
_, ImportDeclarationType
importDeclType, Maybe ModuleName
_, Map
  (ProperName 'TypeName)
  ([ProperName 'ConstructorName], ExportSource)
exportedTypes) =
    case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ProperName 'TypeName
newtypeName Map
  (ProperName 'TypeName)
  ([ProperName 'ConstructorName], ExportSource)
exportedTypes of
      Just ([ProperName 'ConstructorName
_], ExportSource
_) -> case ImportDeclarationType
importDeclType of
        ImportDeclarationType
Implicit -> Bool
True
        Explicit [DeclarationRef]
refs -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any DeclarationRef -> Bool
isNewtypeCtorRef [DeclarationRef]
refs
        Hiding [DeclarationRef]
refs -> Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any DeclarationRef -> Bool
isNewtypeCtorRef [DeclarationRef]
refs
      Maybe ([ProperName 'ConstructorName], ExportSource)
_ -> Bool
False
  isNewtypeCtorRef :: DeclarationRef -> Bool
isNewtypeCtorRef = \case
    TypeRef SourceSpan
_ ProperName 'TypeName
importedTyName Maybe [ProperName 'ConstructorName]
Nothing -> ProperName 'TypeName
importedTyName forall a. Eq a => a -> a -> Bool
== ProperName 'TypeName
newtypeName
    TypeRef SourceSpan
_ ProperName 'TypeName
importedTyName (Just [ProperName 'ConstructorName
_]) -> ProperName 'TypeName
importedTyName forall a. Eq a => a -> a -> Bool
== ProperName 'TypeName
newtypeName
    DeclarationRef
_ -> Bool
False

-- | Constraints of the form @Coercible (N a_0 .. a_n) b@ yield a constraint
-- @Coercible a b@ if unwraping the newtype yields @a@.
canonNewtypeLeft
  :: MonadState CheckState m
  => MonadWriter [ErrorMessageHint] m
  => Environment
  -> SourceType
  -> SourceType
  -> MaybeT m Canonicalized
canonNewtypeLeft :: forall (m :: * -> *).
(MonadState CheckState m, MonadWriter [ErrorMessageHint] m) =>
Environment -> SourceType -> SourceType -> MaybeT m Canonicalized
canonNewtypeLeft Environment
env SourceType
a SourceType
b =
  forall (m :: * -> *).
(MonadState CheckState m, MonadWriter [ErrorMessageHint] m) =>
Environment
-> SourceType -> m (Either UnwrapNewtypeError SourceType)
unwrapNewtype Environment
env SourceType
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left UnwrapNewtypeError
CannotUnwrapInfiniteNewtypeChain -> forall (f :: * -> *) a. Alternative f => f a
empty
    Left UnwrapNewtypeError
CannotUnwrapConstructor -> forall (f :: * -> *) a. Alternative f => f a
empty
    Right SourceType
a' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (SourceType, SourceType) -> Canonicalized
Canonicalized forall a b. (a -> b) -> a -> b
$ forall a. a -> Set a
S.singleton (SourceType
a', SourceType
b)

-- | Constraints of the form @Coercible a (N b_0 .. b_n)@ yield a constraint
-- @Coercible a b@ if unwraping the newtype yields @b@.
canonNewtypeRight
  :: MonadState CheckState m
  => MonadWriter [ErrorMessageHint] m
  => Environment
  -> SourceType
  -> SourceType
  -> MaybeT m Canonicalized
canonNewtypeRight :: forall (m :: * -> *).
(MonadState CheckState m, MonadWriter [ErrorMessageHint] m) =>
Environment -> SourceType -> SourceType -> MaybeT m Canonicalized
canonNewtypeRight Environment
env =
  forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadState CheckState m, MonadWriter [ErrorMessageHint] m) =>
Environment -> SourceType -> SourceType -> MaybeT m Canonicalized
canonNewtypeLeft Environment
env

-- | Decomposes constraints of the form @Coercible (D a_0 .. a_n) (D b_0 .. b_n)@
-- into constraints on their representational arguments, ignoring phantom
-- arguments and failing on unequal nominal arguments.
--
-- For instance given the declarations:
--
-- @
-- data D a b c = D a b
-- type role D nominal representational phantom
-- @
--
-- We can decompose @Coercible (D a b d) (D a c e)@ into @Coercible b c@, but
-- decomposing @Coercible (D a c d) (D b c d)@ would fail.
decompose
  :: MonadError MultipleErrors m
  => Environment
  -> Qualified (ProperName 'TypeName)
  -> [SourceType]
  -> [SourceType]
  -> m Canonicalized
decompose :: forall (m :: * -> *).
MonadError MultipleErrors m =>
Environment
-> Qualified (ProperName 'TypeName)
-> [SourceType]
-> [SourceType]
-> m Canonicalized
decompose Environment
env Qualified (ProperName 'TypeName)
tyName [SourceType]
axs [SourceType]
bxs = do
  let roles :: [Role]
roles = Environment -> Qualified (ProperName 'TypeName) -> [Role]
lookupRoles Environment
env Qualified (ProperName 'TypeName)
tyName
      f :: Role
-> SourceType -> SourceType -> f (Set (SourceType, SourceType))
f Role
role SourceType
ax SourceType
bx = case Role
role of
        Role
Nominal
          -- If we had first-class equality constraints, we'd just
          -- emit one of the form @(a ~ b)@ here and let the solver
          -- recurse. Since we don't we must compare the types at
          -- this point and fail if they don't match. This likely
          -- means there are cases we should be able to handle that
          -- we currently can't, but is at least sound.
          | SourceType
ax forall a. Eq a => a -> a -> Bool
== SourceType
bx ->
              forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
          | Bool
otherwise ->
              forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> SimpleErrorMessage
TypesDoNotUnify SourceType
ax SourceType
bx
        Role
Representational ->
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Set a
S.singleton (SourceType
ax, SourceType
bx)
        Role
Phantom ->
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Set (SourceType, SourceType) -> Canonicalized
Canonicalized forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$ forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 forall {f :: * -> *}.
MonadError MultipleErrors f =>
Role
-> SourceType -> SourceType -> f (Set (SourceType, SourceType))
f [Role]
roles [SourceType]
axs [SourceType]
bxs

-- | Constraints of the form @Coercible (D a_0 .. a_n) (D b_0 .. b_n)@, where
-- @D@ is not a newtype, yield constraints on their arguments.
canonDecomposition
  :: MonadError MultipleErrors m
  => MonadState CheckState m
  => Environment
  -> SourceType
  -> SourceType
  -> MaybeT m Canonicalized
canonDecomposition :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Environment -> SourceType -> SourceType -> MaybeT m Canonicalized
canonDecomposition Environment
env SourceType
a SourceType
b
  | (TypeConstructor SourceAnn
_ Qualified (ProperName 'TypeName)
aTyName, [SourceType]
_, [SourceType]
axs) <- forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes SourceType
a
  , (TypeConstructor SourceAnn
_ Qualified (ProperName 'TypeName)
bTyName, [SourceType]
_, [SourceType]
bxs) <- forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes SourceType
b
  , Qualified (ProperName 'TypeName)
aTyName forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
bTyName
  , Maybe ([Text], ProperName 'ConstructorName, SourceType)
Nothing <- Environment
-> Qualified (ProperName 'TypeName)
-> [SourceType]
-> Maybe ([Text], ProperName 'ConstructorName, SourceType)
lookupNewtypeConstructor Environment
env Qualified (ProperName 'TypeName)
aTyName [] =
      forall (m :: * -> *).
MonadError MultipleErrors m =>
Environment
-> Qualified (ProperName 'TypeName)
-> [SourceType]
-> [SourceType]
-> m Canonicalized
decompose Environment
env Qualified (ProperName 'TypeName)
aTyName [SourceType]
axs [SourceType]
bxs
  | Bool
otherwise = forall (f :: * -> *) a. Alternative f => f a
empty

-- | Constraints of the form @Coercible (D1 a_0 .. a_n) (D2 b_0 .. b_n)@, where
-- @D1@ and @D2@ are different type constructors and neither of them are
-- newtypes, are insoluble.
canonDecompositionFailure
  :: MonadError MultipleErrors m
  => MonadState CheckState m
  => Environment
  -> SourceType
  -> SourceType
  -> SourceType
  -> MaybeT m Canonicalized
canonDecompositionFailure :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Environment
-> SourceType -> SourceType -> SourceType -> MaybeT m Canonicalized
canonDecompositionFailure Environment
env SourceType
k SourceType
a SourceType
b
  | (TypeConstructor SourceAnn
_ Qualified (ProperName 'TypeName)
aTyName, [SourceType]
_, [SourceType]
_) <- forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes SourceType
a
  , (TypeConstructor SourceAnn
_ Qualified (ProperName 'TypeName)
bTyName, [SourceType]
_, [SourceType]
_) <- forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes SourceType
b
  , Qualified (ProperName 'TypeName)
aTyName forall a. Eq a => a -> a -> Bool
/= Qualified (ProperName 'TypeName)
bTyName
  , Maybe ([Text], ProperName 'ConstructorName, SourceType)
Nothing <- Environment
-> Qualified (ProperName 'TypeName)
-> [SourceType]
-> Maybe ([Text], ProperName 'ConstructorName, SourceType)
lookupNewtypeConstructor Environment
env Qualified (ProperName 'TypeName)
aTyName []
  , Maybe ([Text], ProperName 'ConstructorName, SourceType)
Nothing <- Environment
-> Qualified (ProperName 'TypeName)
-> [SourceType]
-> Maybe ([Text], ProperName 'ConstructorName, SourceType)
lookupNewtypeConstructor Environment
env Qualified (ProperName 'TypeName)
bTyName [] =
      forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> SourceType -> MultipleErrors
insoluble SourceType
k SourceType
a SourceType
b
  | Bool
otherwise = forall (f :: * -> *) a. Alternative f => f a
empty

-- | Wanted constraints of the form @Coercible (N a_0 .. a_n) (N b_0 .. b_n)@,
-- where @N@ is a newtype whose constructor is out of scope, yield constraints
-- on their arguments only when no given constraint can discharge them.
--
-- We cannot decompose given constraints because newtypes are not necessarily
-- injective with respect to representational equality.
--
-- For instance given the declaration:
--
-- @
-- newtype Const a b = MkConst a
-- type role Const representational representational
-- @
--
-- Decomposing a given @Coercible (Const a a) (Const a b)@ constraint to
-- @Coercible a b@ when @MkConst@ is out of scope would let us coerce arbitrary
-- types in modules where @MkConst@ is imported, because the given is easily
-- satisfied with the newtype unwraping rules.
--
-- Moreover we do not decompose wanted constraints if they could be discharged
-- by a given constraint.
--
-- For instance the declaration:
--
-- @
-- example :: forall a b. Coercible (Const a a) (Const a b) => Const a a -> Const a b
-- example = coerce
-- @
--
-- yield an irreducible given @Coercible (Const a a) (Const a b)@ when @MkConst@
-- is out of scope. Would we decompose the wanted
-- @Coercible (Const a a) (Const a b)@ to @Coercible a b@ we would not be able
-- to discharge it with the given.
canonNewtypeDecomposition
  :: MonadError MultipleErrors m
  => MonadState CheckState m
  => Environment
  -> Maybe [(SourceType, SourceType, SourceType)]
  -> SourceType
  -> SourceType
  -> MaybeT m Canonicalized
canonNewtypeDecomposition :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Environment
-> Maybe [(SourceType, SourceType, SourceType)]
-> SourceType
-> SourceType
-> MaybeT m Canonicalized
canonNewtypeDecomposition Environment
env (Just [(SourceType, SourceType, SourceType)]
givens) SourceType
a SourceType
b
  | (TypeConstructor SourceAnn
_ Qualified (ProperName 'TypeName)
aTyName, [SourceType]
_, [SourceType]
axs) <- forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes SourceType
a
  , (TypeConstructor SourceAnn
_ Qualified (ProperName 'TypeName)
bTyName, [SourceType]
_, [SourceType]
bxs) <- forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes SourceType
b
  , Qualified (ProperName 'TypeName)
aTyName forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
bTyName
  , Just ([Text], ProperName 'ConstructorName, SourceType)
_ <- Environment
-> Qualified (ProperName 'TypeName)
-> [SourceType]
-> Maybe ([Text], ProperName 'ConstructorName, SourceType)
lookupNewtypeConstructor Environment
env Qualified (ProperName 'TypeName)
aTyName [] = do
      let givensCanDischarge :: Bool
givensCanDischarge = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(SourceType, SourceType, SourceType)
given -> (SourceType, SourceType, SourceType)
-> (SourceType, SourceType) -> Bool
canDischarge (SourceType, SourceType, SourceType)
given (SourceType
a, SourceType
b)) [(SourceType, SourceType, SourceType)]
givens
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
givensCanDischarge
      forall (m :: * -> *).
MonadError MultipleErrors m =>
Environment
-> Qualified (ProperName 'TypeName)
-> [SourceType]
-> [SourceType]
-> m Canonicalized
decompose Environment
env Qualified (ProperName 'TypeName)
aTyName [SourceType]
axs [SourceType]
bxs
canonNewtypeDecomposition Environment
_ Maybe [(SourceType, SourceType, SourceType)]
_ SourceType
_ SourceType
_ = forall (f :: * -> *) a. Alternative f => f a
empty

-- | Constraints of the form @Coercible (N1 a_0 .. a_n) (N2 b_0 .. b_n)@, where
-- @N1@ and @N2@ are different type constructors and either of them is a
-- newtype whose constructor is out of scope, are irreducible.
canonNewtypeDecompositionFailure
  :: Monad m
  => SourceType
  -> SourceType
  -> MaybeT m Canonicalized
canonNewtypeDecompositionFailure :: forall (m :: * -> *).
Monad m =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonNewtypeDecompositionFailure SourceType
a SourceType
b
  | (TypeConstructor{}, [SourceType]
_, [SourceType]
_) <- forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes SourceType
a
  , (TypeConstructor{}, [SourceType]
_, [SourceType]
_) <- forall a. Type a -> (Type a, [Type a], [Type a])
unapplyTypes SourceType
b
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure Canonicalized
Irreducible
  | Bool
otherwise = forall (f :: * -> *) a. Alternative f => f a
empty

-- | Constraints of the form @Coercible tv1 tv2@ may be irreducibles, but only
-- when the variables are lexicographically ordered. Reordering variables is
-- necessary to prevent loops.
--
-- For instance the declaration:
--
-- @
-- example :: forall a b. Coercible a b => Coercible b a => a -> b
-- example = coerce
-- @
--
-- yields the irreducible givens @Coercible a b@ and @Coercible b a@ which would
-- repeatedly kick each other out the inert set whereas reordering the latter to
-- @Coercible a b@ makes it redundant and let us discharge it.
canonTypeVars
  :: Monad m
  => SourceType
  -> SourceType
  -> MaybeT m Canonicalized
canonTypeVars :: forall (m :: * -> *).
Monad m =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonTypeVars SourceType
a SourceType
b
  | Skolem SourceAnn
_ Text
tv1 Maybe SourceType
_ Int
_ SkolemScope
_ <- SourceType
a
  , Skolem SourceAnn
_ Text
tv2 Maybe SourceType
_ Int
_ SkolemScope
_ <- SourceType
b
  , Text
tv2 forall a. Ord a => a -> a -> Bool
< Text
tv1
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (SourceType, SourceType) -> Canonicalized
Canonicalized forall a b. (a -> b) -> a -> b
$ forall a. a -> Set a
S.singleton (SourceType
b, SourceType
a)
  | Skolem{} <- SourceType
a, Skolem{} <- SourceType
b
  = forall (f :: * -> *) a. Applicative f => a -> f a
pure Canonicalized
Irreducible
  | Bool
otherwise = forall (f :: * -> *) a. Alternative f => f a
empty

-- | Constraints of the form @Coercible tv ty@ are irreducibles.
canonTypeVarLeft
  :: Monad m
  => SourceType
  -> SourceType
  -> MaybeT m Canonicalized
canonTypeVarLeft :: forall (m :: * -> *).
Monad m =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonTypeVarLeft SourceType
a SourceType
_
  | Skolem{} <- SourceType
a = forall (f :: * -> *) a. Applicative f => a -> f a
pure Canonicalized
Irreducible
  | Bool
otherwise = forall (f :: * -> *) a. Alternative f => f a
empty

-- | Constraints of the form @Coercible ty tv@ are reordered to
-- @Coercible tv ty@ to satisfy the canonicality requirement of having the type
-- variable on the left.
canonTypeVarRight
  :: Monad m
  => SourceType
  -> SourceType
  -> MaybeT m Canonicalized
canonTypeVarRight :: forall (m :: * -> *).
Monad m =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonTypeVarRight SourceType
a SourceType
b
  | Skolem{} <- SourceType
b = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (SourceType, SourceType) -> Canonicalized
Canonicalized forall a b. (a -> b) -> a -> b
$ forall a. a -> Set a
S.singleton (SourceType
b, SourceType
a)
  | Bool
otherwise = forall (f :: * -> *) a. Alternative f => f a
empty

-- | Constraints of the form @Coercible (f a_0 .. a_n) b@ are irreducibles.
canonApplicationLeft
  :: Monad m
  => SourceType
  -> SourceType
  -> MaybeT m Canonicalized
canonApplicationLeft :: forall (m :: * -> *).
Monad m =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonApplicationLeft SourceType
a SourceType
_
  | TypeApp{} <- SourceType
a = forall (f :: * -> *) a. Applicative f => a -> f a
pure Canonicalized
Irreducible
  | Bool
otherwise = forall (f :: * -> *) a. Alternative f => f a
empty

-- | Constraints of the form @Coercible a (f b_0 .. b_n) b@ are irreducibles.
canonApplicationRight
  :: Monad m
  => SourceType
  -> SourceType
  -> MaybeT m Canonicalized
canonApplicationRight :: forall (m :: * -> *).
Monad m =>
SourceType -> SourceType -> MaybeT m Canonicalized
canonApplicationRight SourceType
_ SourceType
b
  | TypeApp{} <- SourceType
b = forall (f :: * -> *) a. Applicative f => a -> f a
pure Canonicalized
Irreducible
  | Bool
otherwise = forall (f :: * -> *) a. Alternative f => f a
empty