{-# LANGUAGE DuplicateRecordFields #-}
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
data GivenSolverState =
GivenSolverState
{ GivenSolverState -> [(SourceType, SourceType, SourceType)]
inertGivens :: [(SourceType, SourceType, SourceType)]
, GivenSolverState -> [(SourceType, SourceType)]
unsolvedGivens :: [(SourceType, SourceType)]
}
initialGivenSolverState :: [(SourceType, SourceType)] -> GivenSolverState
initialGivenSolverState :: [(SourceType, SourceType)] -> GivenSolverState
initialGivenSolverState =
[(SourceType, SourceType, SourceType)]
-> [(SourceType, SourceType)] -> GivenSolverState
GivenSolverState []
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
data WantedSolverState =
WantedSolverState
{ WantedSolverState -> [(SourceType, SourceType, SourceType)]
inertGivens :: [(SourceType, SourceType, SourceType)]
, WantedSolverState -> [(SourceType, SourceType, SourceType)]
inertWanteds :: [(SourceType, SourceType, SourceType)]
, WantedSolverState -> [(SourceType, SourceType)]
unsolvedWanteds :: [(SourceType, SourceType)]
}
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)]
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
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'
)
data Interaction
= Simplified (SourceType, SourceType)
| Discharged
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
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
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
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
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
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
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
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
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
data Canonicalized
= Canonicalized (S.Set (SourceType, SourceType))
| Irreducible
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
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 =
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])
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
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
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
([(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
data UnwrapNewtypeError
= CannotUnwrapInfiniteNewtypeChain
| CannotUnwrapConstructor
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
, 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 }
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)
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
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)
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
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
| 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
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
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
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
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
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
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
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
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
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