{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
module Disco.Typecheck.Solve where
import Unbound.Generics.LocallyNameless (
Alpha,
Name,
Subst,
fv,
name2Integer,
string2Name,
substs,
)
import Data.Coerce
import GHC.Generics (Generic)
import Control.Arrow ((&&&), (***))
import Control.Lens hiding (use, (%=), (.=))
import Control.Monad (unless, zipWithM)
import Data.Bifunctor (first, second)
import Data.Either (partitionEithers)
import Data.List (
find,
foldl',
intersect,
partition,
)
import Data.Map (Map, (!))
import qualified Data.Map as M
import Data.Maybe (
fromJust,
fromMaybe,
mapMaybe,
)
import Data.Monoid (First (..))
import Data.Set (Set)
import qualified Data.Set as S
import Data.Tuple
import Disco.Effects.Fresh
import Disco.Effects.State
import Polysemy
import Polysemy.Error
import Polysemy.Input
import Polysemy.Output
import Disco.Messages
import Disco.Pretty hiding ((<>))
import Disco.Subst
import qualified Disco.Subst as Subst
import Disco.Typecheck.Constraints
import Disco.Typecheck.Graph (Graph)
import qualified Disco.Typecheck.Graph as G
import Disco.Typecheck.Unify
import Disco.Types
import Disco.Types.Qualifiers
import Disco.Types.Rules
data SolveError where
NoWeakUnifier :: SolveError
NoUnify :: SolveError
UnqualBase :: Qualifier -> BaseTy -> SolveError
Unqual :: Qualifier -> Type -> SolveError
QualSkolem :: Qualifier -> Name Type -> SolveError
deriving (Int -> SolveError -> ShowS
[SolveError] -> ShowS
SolveError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SolveError] -> ShowS
$cshowList :: [SolveError] -> ShowS
show :: SolveError -> String
$cshow :: SolveError -> String
showsPrec :: Int -> SolveError -> ShowS
$cshowsPrec :: Int -> SolveError -> ShowS
Show)
instance Semigroup SolveError where
SolveError
e <> :: SolveError -> SolveError -> SolveError
<> SolveError
_ = SolveError
e
runSolve :: Sem (Fresh ': Error SolveError ': r) a -> Sem r (Either SolveError a)
runSolve :: forall (r :: [(* -> *) -> * -> *]) a.
Sem (Fresh : Error SolveError : r) a -> Sem r (Either SolveError a)
runSolve = forall e (r :: [(* -> *) -> * -> *]) a.
Sem (Error e : r) a -> Sem r (Either e a)
runError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: [(* -> *) -> * -> *]) a. Sem (Fresh : r) a -> Sem r a
runFresh
filterErrors :: Member (Error e) r => [Sem r a] -> Sem r [a]
filterErrors :: forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
[Sem r a] -> Sem r [a]
filterErrors [Sem r a]
ms = do
[Either e a]
es <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
Sem r a -> Sem r (Either e a)
try [Sem r a]
ms
case forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either e a]
es of
(e
e : [e]
_, []) -> forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw e
e
([e]
_, [a]
as) -> forall (m :: * -> *) a. Monad m => a -> m a
return [a]
as
asum' :: Member (Error e) r => [Sem r a] -> Sem r a
asum' :: forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
[Sem r a] -> Sem r a
asum' [] = forall a. HasCallStack => String -> a
error String
"Impossible: asum' []"
asum' [Sem r a
m] = Sem r a
m
asum' (Sem r a
m : [Sem r a]
ms) = Sem r a
m forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
Sem r a -> (e -> Sem r a) -> Sem r a
`catch` (\e
_ -> forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
[Sem r a] -> Sem r a
asum' [Sem r a]
ms)
data SimpleConstraint where
(:<:) :: Type -> Type -> SimpleConstraint
(:=:) :: Type -> Type -> SimpleConstraint
deriving (Int -> SimpleConstraint -> ShowS
[SimpleConstraint] -> ShowS
SimpleConstraint -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SimpleConstraint] -> ShowS
$cshowList :: [SimpleConstraint] -> ShowS
show :: SimpleConstraint -> String
$cshow :: SimpleConstraint -> String
showsPrec :: Int -> SimpleConstraint -> ShowS
$cshowsPrec :: Int -> SimpleConstraint -> ShowS
Show, SimpleConstraint -> SimpleConstraint -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SimpleConstraint -> SimpleConstraint -> Bool
$c/= :: SimpleConstraint -> SimpleConstraint -> Bool
== :: SimpleConstraint -> SimpleConstraint -> Bool
$c== :: SimpleConstraint -> SimpleConstraint -> Bool
Eq, Eq SimpleConstraint
SimpleConstraint -> SimpleConstraint -> Bool
SimpleConstraint -> SimpleConstraint -> Ordering
SimpleConstraint -> SimpleConstraint -> SimpleConstraint
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SimpleConstraint -> SimpleConstraint -> SimpleConstraint
$cmin :: SimpleConstraint -> SimpleConstraint -> SimpleConstraint
max :: SimpleConstraint -> SimpleConstraint -> SimpleConstraint
$cmax :: SimpleConstraint -> SimpleConstraint -> SimpleConstraint
>= :: SimpleConstraint -> SimpleConstraint -> Bool
$c>= :: SimpleConstraint -> SimpleConstraint -> Bool
> :: SimpleConstraint -> SimpleConstraint -> Bool
$c> :: SimpleConstraint -> SimpleConstraint -> Bool
<= :: SimpleConstraint -> SimpleConstraint -> Bool
$c<= :: SimpleConstraint -> SimpleConstraint -> Bool
< :: SimpleConstraint -> SimpleConstraint -> Bool
$c< :: SimpleConstraint -> SimpleConstraint -> Bool
compare :: SimpleConstraint -> SimpleConstraint -> Ordering
$ccompare :: SimpleConstraint -> SimpleConstraint -> Ordering
Ord, forall x. Rep SimpleConstraint x -> SimpleConstraint
forall x. SimpleConstraint -> Rep SimpleConstraint x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SimpleConstraint x -> SimpleConstraint
$cfrom :: forall x. SimpleConstraint -> Rep SimpleConstraint x
Generic, Show SimpleConstraint
AlphaCtx -> NthPatFind -> SimpleConstraint -> SimpleConstraint
AlphaCtx -> NamePatFind -> SimpleConstraint -> SimpleConstraint
AlphaCtx -> Perm AnyName -> SimpleConstraint -> SimpleConstraint
AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Bool
AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Ordering
SimpleConstraint -> Bool
SimpleConstraint -> All
SimpleConstraint -> DisjointSet AnyName
SimpleConstraint -> NthPatFind
SimpleConstraint -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> SimpleConstraint -> f SimpleConstraint
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> SimpleConstraint -> m (SimpleConstraint, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> SimpleConstraint
-> (SimpleConstraint -> Perm AnyName -> m b)
-> m b
acompare' :: AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Ordering
$cacompare' :: AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> SimpleConstraint -> m (SimpleConstraint, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> SimpleConstraint -> m (SimpleConstraint, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> SimpleConstraint
-> (SimpleConstraint -> Perm AnyName -> m b)
-> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> SimpleConstraint
-> (SimpleConstraint -> Perm AnyName -> m b)
-> m b
swaps' :: AlphaCtx -> Perm AnyName -> SimpleConstraint -> SimpleConstraint
$cswaps' :: AlphaCtx -> Perm AnyName -> SimpleConstraint -> SimpleConstraint
namePatFind :: SimpleConstraint -> NamePatFind
$cnamePatFind :: SimpleConstraint -> NamePatFind
nthPatFind :: SimpleConstraint -> NthPatFind
$cnthPatFind :: SimpleConstraint -> NthPatFind
isEmbed :: SimpleConstraint -> Bool
$cisEmbed :: SimpleConstraint -> Bool
isTerm :: SimpleConstraint -> All
$cisTerm :: SimpleConstraint -> All
isPat :: SimpleConstraint -> DisjointSet AnyName
$cisPat :: SimpleConstraint -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> SimpleConstraint -> SimpleConstraint
$copen :: AlphaCtx -> NthPatFind -> SimpleConstraint -> SimpleConstraint
close :: AlphaCtx -> NamePatFind -> SimpleConstraint -> SimpleConstraint
$cclose :: AlphaCtx -> NamePatFind -> SimpleConstraint -> SimpleConstraint
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> SimpleConstraint -> f SimpleConstraint
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> SimpleConstraint -> f SimpleConstraint
aeq' :: AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Bool
$caeq' :: AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Bool
Alpha, Subst Type)
instance Pretty SimpleConstraint where
pretty :: forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
SimpleConstraint -> Sem r (Doc ann)
pretty = \case
Type
ty1 :<: Type
ty2 -> forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty1 forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"<:" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty2
Type
ty1 :=: Type
ty2 -> forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty1 forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"=" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty2
data TyVarInfo = TVI
{ TyVarInfo -> First Ilk
_tyVarIlk :: First Ilk
, TyVarInfo -> Sort
_tyVarSort :: Sort
}
deriving (Int -> TyVarInfo -> ShowS
[TyVarInfo] -> ShowS
TyVarInfo -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TyVarInfo] -> ShowS
$cshowList :: [TyVarInfo] -> ShowS
show :: TyVarInfo -> String
$cshow :: TyVarInfo -> String
showsPrec :: Int -> TyVarInfo -> ShowS
$cshowsPrec :: Int -> TyVarInfo -> ShowS
Show)
makeLenses ''TyVarInfo
instance Pretty TyVarInfo where
pretty :: forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
TyVarInfo -> Sem r (Doc ann)
pretty (TVI (First Maybe Ilk
ilk) Sort
s) = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc ann
"?") forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Maybe Ilk
ilk forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ann)
"%" forall a. Semigroup a => a -> a -> a
<> forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Sort
s
mkTVI :: Ilk -> Sort -> TyVarInfo
mkTVI :: Ilk -> Sort -> TyVarInfo
mkTVI = First Ilk -> Sort -> TyVarInfo
TVI forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Maybe a -> First a
First forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just
instance Semigroup TyVarInfo where
TVI First Ilk
i1 Sort
s1 <> :: TyVarInfo -> TyVarInfo -> TyVarInfo
<> TVI First Ilk
i2 Sort
s2 = First Ilk -> Sort -> TyVarInfo
TVI (First Ilk
i1 forall a. Semigroup a => a -> a -> a
<> First Ilk
i2) (Sort
s1 forall a. Semigroup a => a -> a -> a
<> Sort
s2)
newtype TyVarInfoMap = VM {TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM :: Map (Name Type) TyVarInfo}
deriving (Int -> TyVarInfoMap -> ShowS
[TyVarInfoMap] -> ShowS
TyVarInfoMap -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TyVarInfoMap] -> ShowS
$cshowList :: [TyVarInfoMap] -> ShowS
show :: TyVarInfoMap -> String
$cshow :: TyVarInfoMap -> String
showsPrec :: Int -> TyVarInfoMap -> ShowS
$cshowsPrec :: Int -> TyVarInfoMap -> ShowS
Show)
instance Pretty TyVarInfoMap where
pretty :: forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
TyVarInfoMap -> Sem r (Doc ann)
pretty (VM Map (Name Type) TyVarInfo
m) = forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Map (Name Type) TyVarInfo
m
onVM ::
(Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo) ->
TyVarInfoMap ->
TyVarInfoMap
onVM :: (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap -> TyVarInfoMap
onVM Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo
f (VM Map (Name Type) TyVarInfo
m) = Map (Name Type) TyVarInfo -> TyVarInfoMap
VM (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo
f Map (Name Type) TyVarInfo
m)
lookupVM :: Name Type -> TyVarInfoMap -> Maybe TyVarInfo
lookupVM :: Name Type -> TyVarInfoMap -> Maybe TyVarInfo
lookupVM Name Type
v = forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name Type
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM
deleteVM :: Name Type -> TyVarInfoMap -> TyVarInfoMap
deleteVM :: Name Type -> TyVarInfoMap -> TyVarInfoMap
deleteVM = (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap -> TyVarInfoMap
onVM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Map k a
M.delete
addSkolems :: [Name Type] -> TyVarInfoMap -> TyVarInfoMap
addSkolems :: [Name Type] -> TyVarInfoMap -> TyVarInfoMap
addSkolems [Name Type]
vs = (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap -> TyVarInfoMap
onVM forall a b. (a -> b) -> a -> b
$ \Map (Name Type) TyVarInfo
vm -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip (\Name Type
v -> forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name Type
v (Ilk -> Sort -> TyVarInfo
mkTVI Ilk
Skolem forall a. Monoid a => a
mempty))) Map (Name Type) TyVarInfo
vm [Name Type]
vs
instance Semigroup TyVarInfoMap where
VM Map (Name Type) TyVarInfo
sm1 <> :: TyVarInfoMap -> TyVarInfoMap -> TyVarInfoMap
<> VM Map (Name Type) TyVarInfo
sm2 = Map (Name Type) TyVarInfo -> TyVarInfoMap
VM (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. Semigroup a => a -> a -> a
(<>) Map (Name Type) TyVarInfo
sm1 Map (Name Type) TyVarInfo
sm2)
instance Monoid TyVarInfoMap where
mempty :: TyVarInfoMap
mempty = Map (Name Type) TyVarInfo -> TyVarInfoMap
VM forall k a. Map k a
M.empty
mappend :: TyVarInfoMap -> TyVarInfoMap -> TyVarInfoMap
mappend = forall a. Semigroup a => a -> a -> a
(<>)
getSort :: TyVarInfoMap -> Name Type -> Sort
getSort :: TyVarInfoMap -> Name Type -> Sort
getSort (VM Map (Name Type) TyVarInfo
m) Name Type
v = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sort
topSort (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Lens' TyVarInfo Sort
tyVarSort) (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name Type
v Map (Name Type) TyVarInfo
m)
getIlk :: TyVarInfoMap -> Name Type -> Maybe Ilk
getIlk :: TyVarInfoMap -> Name Type -> Maybe Ilk
getIlk (VM Map (Name Type) TyVarInfo
m) Name Type
v = (Map (Name Type) TyVarInfo
m forall s a. s -> Getting (First a) s a -> Maybe a
^? forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Name Type
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TyVarInfo (First Ilk)
tyVarIlk) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. First a -> Maybe a
getFirst
extendSort :: Name Type -> Sort -> TyVarInfoMap -> TyVarInfoMap
extendSort :: Name Type -> Sort -> TyVarInfoMap -> TyVarInfoMap
extendSort Name Type
x Sort
s = (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap -> TyVarInfoMap
onVM (forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Name Type
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Prism (Maybe a) (Maybe b) a b
_Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TyVarInfo Sort
tyVarSort forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall a. Ord a => Set a -> Set a -> Set a
`S.union` Sort
s))
data SimplifyState = SS
{ SimplifyState -> TyVarInfoMap
_ssVarMap :: TyVarInfoMap
, SimplifyState -> [SimpleConstraint]
_ssConstraints :: [SimpleConstraint]
, SimplifyState -> S
_ssSubst :: S
, SimplifyState -> Set SimpleConstraint
_ssSeen :: Set SimpleConstraint
}
makeLenses ''SimplifyState
lkup :: (Ord k, Show k, Show (Map k a)) => String -> Map k a -> k -> a
lkup :: forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
messg Map k a
m k
k = forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
error String
errMsg) (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup k
k Map k a
m)
where
errMsg :: String
errMsg =
[String] -> String
unlines
[ String
"Key lookup error:"
, String
" Key = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show k
k
, String
" Map = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Map k a
m
, String
" Location: " forall a. [a] -> [a] -> [a]
++ String
messg
]
solveConstraint ::
Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx] r =>
Constraint ->
Sem r S
solveConstraint :: forall ann (r :: [(* -> *) -> * -> *]).
Members
'[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx]
r =>
Constraint -> Sem r S
solveConstraint Constraint
c = do
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Solving:"
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty Constraint
c
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"------------------------------"
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Decomposing constraints..."
[(TyVarInfoMap, [SimpleConstraint])]
qcList <- forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint Constraint
c
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
[Sem r a] -> Sem r a
asum' (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall ann (r :: [(* -> *) -> * -> *]).
Members
'[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx]
r =>
TyVarInfoMap -> [SimpleConstraint] -> Sem r S
solveConstraintChoice) [(TyVarInfoMap, [SimpleConstraint])]
qcList)
solveConstraintChoice ::
Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx] r =>
TyVarInfoMap ->
[SimpleConstraint] ->
Sem r S
solveConstraintChoice :: forall ann (r :: [(* -> *) -> * -> *]).
Members
'[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx]
r =>
TyVarInfoMap -> [SimpleConstraint] -> Sem r S
solveConstraintChoice TyVarInfoMap
quals [SimpleConstraint]
cs = do
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
quals
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: [(* -> *) -> * -> *]) ann.
Pretty t =>
t -> Sem r (Doc ann)
pretty' [SimpleConstraint]
cs)
TyDefCtx
tyDefns <- forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
let toEqn :: SimpleConstraint -> (Type, Type)
toEqn (Type
t1 :<: Type
t2) = (Type
t1, Type
t2)
toEqn (Type
t1 :=: Type
t2) = (Type
t1, Type
t2)
S
_ <- forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Maybe a -> Sem r a
note SolveError
NoWeakUnifier forall a b. (a -> b) -> a -> b
$ TyDefCtx -> [(Type, Type)] -> Maybe S
weakUnify TyDefCtx
tyDefns (forall a b. (a -> b) -> [a] -> [b]
map SimpleConstraint -> (Type, Type)
toEqn [SimpleConstraint]
cs)
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"------------------------------"
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Running simplifier..."
(TyVarInfoMap
vm, [(Atom, Atom)]
atoms, S
theta_simp) <- forall ann (r :: [(* -> *) -> * -> *]).
Members
'[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
TyVarInfoMap
-> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
simplify TyVarInfoMap
quals [SimpleConstraint]
cs
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Done running simplifier. Results:"
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
vm
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t (r :: [(* -> *) -> * -> *]) ann.
Pretty t =>
t -> Sem r (Doc ann)
pretty' forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Atom
x, Atom
y) -> Atom -> Type
TyAtom Atom
x Type -> Type -> SimpleConstraint
:<: Atom -> Type
TyAtom Atom
y)) [(Atom, Atom)]
atoms
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_simp
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"------------------------------"
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Generating constraint graph..."
let mkAVar :: (Name Type, First Ilk) -> Atom
mkAVar (Name Type
v, First (Just Ilk
Skolem)) = Var -> Atom
AVar (Name Type -> Var
S Name Type
v)
mkAVar (Name Type
v, First Ilk
_) = Var -> Atom
AVar (Name Type -> Var
U Name Type
v)
vars :: Set Atom
vars = forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ((Name Type, First Ilk) -> Atom
mkAVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Lens' TyVarInfo (First Ilk)
tyVarIlk)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
M.assocs forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM forall a b. (a -> b) -> a -> b
$ TyVarInfoMap
vm
g :: Graph Atom
g = forall a. (Show a, Ord a) => Set a -> [(a, a)] -> Graph a
mkConstraintGraph Set Atom
vars [(Atom, Atom)]
atoms
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty Graph Atom
g
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"------------------------------"
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Checking WCCs for skolems..."
(Graph UAtom
g', S
theta_skolem) <- forall ann (r :: [(* -> *) -> * -> *]).
Members
'[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
checkSkolems TyVarInfoMap
vm Graph Atom
g
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_skolem
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"------------------------------"
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Collapsing SCCs..."
(Graph UAtom
g'', S
theta_cyc) <- forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError] r =>
TyDefCtx -> Graph UAtom -> Sem r (Graph UAtom, S)
elimCycles TyDefCtx
tyDefns Graph UAtom
g'
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty Graph UAtom
g''
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_cyc
let sortOK :: (Name Type, Type) -> Bool
sortOK (Name Type
x, TyAtom (ABase BaseTy
ty)) = BaseTy -> Sort -> Bool
hasSort BaseTy
ty (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
x)
sortOK (Name Type
_, TyAtom (AVar (U Name Type
_))) = Bool
True
sortOK (Name Type, Type)
p = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! sortOK " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Name Type, Type)
p
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Name Type, Type) -> Bool
sortOK (forall a. Substitution a -> [(Name a, a)]
Subst.toList S
theta_cyc)) forall a b. (a -> b) -> a -> b
$
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Old sort map:"
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
vm
let vm' :: TyVarInfoMap
vm' = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name Type, Type) -> TyVarInfoMap -> TyVarInfoMap
updateVarMap TyVarInfoMap
vm (forall a. Substitution a -> [(Name a, a)]
Subst.toList S
theta_cyc)
where
updateVarMap :: (Name Type, Type) -> TyVarInfoMap -> TyVarInfoMap
updateVarMap :: (Name Type, Type) -> TyVarInfoMap -> TyVarInfoMap
updateVarMap (Name Type
x, TyAtom (AVar (U Name Type
y))) TyVarInfoMap
vmm = Name Type -> Sort -> TyVarInfoMap -> TyVarInfoMap
extendSort Name Type
y (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vmm Name Type
x) TyVarInfoMap
vmm
updateVarMap (Name Type, Type)
_ TyVarInfoMap
vmm = TyVarInfoMap
vmm
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Updated sort map:"
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
vm
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"------------------------------"
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Checking edges between base types..."
Graph UAtom
g''' <- forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError] r =>
Graph UAtom -> Sem r (Graph UAtom)
checkBaseEdges Graph UAtom
g''
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"------------------------------"
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Solving for type variables..."
S
theta_sol <- forall ann (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output (Message ann)] r =>
TyVarInfoMap -> Graph UAtom -> Sem r S
solveGraph TyVarInfoMap
vm' Graph UAtom
g'''
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_sol
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"------------------------------"
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Composing final substitution..."
let theta_final :: S
theta_final = S
theta_sol forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ S
theta_cyc forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ S
theta_skolem forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ S
theta_simp
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_final
forall (m :: * -> *) a. Monad m => a -> m a
return S
theta_final
decomposeConstraint ::
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint ->
Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint :: forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint (CSub Type
t1 Type
t2) = forall (m :: * -> *) a. Monad m => a -> m a
return [(forall a. Monoid a => a
mempty, [Type
t1 Type -> Type -> SimpleConstraint
:<: Type
t2])]
decomposeConstraint (CEq Type
t1 Type
t2) = forall (m :: * -> *) a. Monad m => a -> m a
return [(forall a. Monoid a => a
mempty, [Type
t1 Type -> Type -> SimpleConstraint
:=: Type
t2])]
decomposeConstraint (CQual Qualifier
q Type
ty) = (forall a. a -> [a] -> [a]
: []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Type -> Qualifier -> Sem r TyVarInfoMap
decomposeQual Type
ty Qualifier
q
decomposeConstraint (CAnd [Constraint]
cs) = forall a b. (a -> b) -> [a] -> [b]
map forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint [Constraint]
cs
decomposeConstraint Constraint
CTrue = forall (m :: * -> *) a. Monad m => a -> m a
return [forall a. Monoid a => a
mempty]
decomposeConstraint (CAll Bind [Name Type] Constraint
ty) = do
([Name Type]
vars, Constraint
c) <- forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind [Name Type] Constraint
ty
let c' :: Constraint
c' = forall b a. Subst b a => [(Name b, b)] -> a -> a
substs ([Name Type] -> [(Name Type, Type)]
mkSkolems [Name Type]
vars) Constraint
c
(forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name Type] -> TyVarInfoMap -> TyVarInfoMap
addSkolems) [Name Type]
vars forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint Constraint
c'
where
mkSkolems :: [Name Type] -> [(Name Type, Type)]
mkSkolems :: [Name Type] -> [(Name Type, Type)]
mkSkolems = forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> a
id forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Name Type -> Type
TySkolem)
decomposeConstraint (COr [Constraint]
cs) = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
[Sem r a] -> Sem r [a]
filterErrors (forall a b. (a -> b) -> [a] -> [b]
map forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint [Constraint]
cs)
decomposeQual ::
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Type ->
Qualifier ->
Sem r TyVarInfoMap
decomposeQual :: forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Type -> Qualifier -> Sem r TyVarInfoMap
decomposeQual = forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go forall a. Set a
S.empty
where
go ::
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier) ->
Type ->
Qualifier ->
Sem r TyVarInfoMap
go :: forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go Set (String, [Type], Qualifier)
_ (TyAtom Atom
a) Qualifier
q = forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError] r =>
Qualifier -> Atom -> Sem r TyVarInfoMap
checkQual Qualifier
q Atom
a
go Set (String, [Type], Qualifier)
seen (TyCon (CUser String
t) [Type]
tys) Qualifier
q = do
case (String
t, [Type]
tys, Qualifier
q) forall a. Ord a => a -> Set a -> Bool
`S.member` Set (String, [Type], Qualifier)
seen of
Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
Bool
False -> do
TyDefCtx
tyDefns <- forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
t TyDefCtx
tyDefns of
Maybe TyDefBody
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show String
t forall a. [a] -> [a] -> [a]
++ String
" not in ty defn map!!"
Just (TyDefBody [String]
_ [Type] -> Type
body) -> do
let ty' :: Type
ty' = [Type] -> Type
body [Type]
tys
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go (forall a. Ord a => a -> Set a -> Set a
S.insert (String
t, [Type]
tys, Qualifier
q) Set (String, [Type], Qualifier)
seen) Type
ty' Qualifier
q
go Set (String, [Type], Qualifier)
seen (TyCon (CContainer (AVar Var
_)) [Type]
tys) Qualifier
q = forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go Set (String, [Type], Qualifier)
seen (Con -> [Type] -> Type
TyCon Con
CList [Type]
tys) Qualifier
q
go Set (String, [Type], Qualifier)
seen ty :: Type
ty@(TyCon Con
c [Type]
tys) Qualifier
q = case Con -> Qualifier -> Maybe [Maybe Qualifier]
qualRules Con
c Qualifier
q of
Maybe [Maybe Qualifier]
Nothing -> forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> SolveError
Unqual Qualifier
q Type
ty
Just [Maybe Qualifier]
qs -> forall a. Monoid a => [a] -> a
mconcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go Set (String, [Type], Qualifier)
seen) [Type]
tys [Maybe Qualifier]
qs
checkQual ::
Members '[Fresh, Error SolveError] r =>
Qualifier ->
Atom ->
Sem r TyVarInfoMap
checkQual :: forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError] r =>
Qualifier -> Atom -> Sem r TyVarInfoMap
checkQual Qualifier
q (AVar (U Name Type
v)) = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Name Type) TyVarInfo -> TyVarInfoMap
VM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. k -> a -> Map k a
M.singleton Name Type
v forall a b. (a -> b) -> a -> b
$ Ilk -> Sort -> TyVarInfo
mkTVI Ilk
Unification (forall a. a -> Set a
S.singleton Qualifier
q)
checkQual Qualifier
q (AVar (S Name Type
v)) = forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ Qualifier -> Name Type -> SolveError
QualSkolem Qualifier
q Name Type
v
checkQual Qualifier
q (ABase BaseTy
bty) =
case BaseTy -> Qualifier -> Bool
hasQual BaseTy
bty Qualifier
q of
Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
Bool
False -> forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ Qualifier -> BaseTy -> SolveError
UnqualBase Qualifier
q BaseTy
bty
simplify ::
Members '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
TyVarInfoMap ->
[SimpleConstraint] ->
Sem r (TyVarInfoMap, [(Atom, Atom)], S)
simplify :: forall ann (r :: [(* -> *) -> * -> *]).
Members
'[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
TyVarInfoMap
-> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
simplify TyVarInfoMap
origVM [SimpleConstraint]
cs =
(\(SS TyVarInfoMap
vm' [SimpleConstraint]
cs' S
s' Set SimpleConstraint
_) -> (TyVarInfoMap
vm', forall a b. (a -> b) -> [a] -> [b]
map SimpleConstraint -> (Atom, Atom)
extractAtoms [SimpleConstraint]
cs', S
s'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]) a.
Integer -> Sem (Fresh : r) a -> Sem r a
runFresh' Integer
n (forall s (r :: [(* -> *) -> * -> *]) a.
s -> Sem (State s : r) a -> Sem r s
execState (TyVarInfoMap
-> [SimpleConstraint] -> S -> Set SimpleConstraint -> SimplifyState
SS TyVarInfoMap
origVM [SimpleConstraint]
cs forall a. Substitution a
idS forall a. Set a
S.empty) forall ann (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError,
Output (Message ann), Input TyDefCtx]
r =>
Sem r ()
simplify')
where
fvNums :: Alpha a => [a] -> [Integer]
fvNums :: forall a. Alpha a => [a] -> [Integer]
fvNums = forall a b. (a -> b) -> [a] -> [b]
map (forall a. Name a -> Integer
name2Integer :: Name Type -> Integer) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf forall a (f :: * -> *) b.
(Alpha a, Typeable b, Contravariant f, Applicative f) =>
(Name b -> f (Name b)) -> a -> f a
fv
n1 :: Integer
n1 = forall {a}. (Num a, Ord a) => [a] -> a
maximum0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Alpha a => [a] -> [Integer]
fvNums forall a b. (a -> b) -> a -> b
$ [SimpleConstraint]
cs
n :: Integer
n = forall a. Enum a => a -> a
succ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer
n1 forall a. a -> [a] -> [a]
:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Alpha a => [a] -> [Integer]
fvNums forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [k]
M.keys forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM forall a b. (a -> b) -> a -> b
$ TyVarInfoMap
origVM
maximum0 :: [a] -> a
maximum0 [] = a
0
maximum0 [a]
xs = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [a]
xs
extractAtoms :: SimpleConstraint -> (Atom, Atom)
extractAtoms :: SimpleConstraint -> (Atom, Atom)
extractAtoms (TyAtom Atom
a1 :<: TyAtom Atom
a2) = (Atom
a1, Atom
a2)
extractAtoms SimpleConstraint
c = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible: simplify left non-atomic or non-subtype constraint " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SimpleConstraint
c
simplify' ::
Members '[State SimplifyState, Fresh, Error SolveError, Output (Message ann), Input TyDefCtx] r =>
Sem r ()
simplify' :: forall ann (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError,
Output (Message ann), Input TyDefCtx]
r =>
Sem r ()
simplify' = do
Maybe SimpleConstraint
mc <- forall (r :: [(* -> *) -> * -> *]).
Members '[State SimplifyState, Fresh, Error SolveError] r =>
Sem r (Maybe SimpleConstraint)
pickSimplifiable
case Maybe SimpleConstraint
mc of
Maybe SimpleConstraint
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just SimpleConstraint
s -> do
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Simplifying:" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: [(* -> *) -> * -> *]) ann.
Pretty t =>
t -> Sem r (Doc ann)
pretty' SimpleConstraint
s
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
SimpleConstraint -> Sem r ()
simplifyOne SimpleConstraint
s
forall ann (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError,
Output (Message ann), Input TyDefCtx]
r =>
Sem r ()
simplify'
pickSimplifiable ::
Members '[State SimplifyState, Fresh, Error SolveError] r =>
Sem r (Maybe SimpleConstraint)
pickSimplifiable :: forall (r :: [(* -> *) -> * -> *]).
Members '[State SimplifyState, Fresh, Error SolveError] r =>
Sem r (Maybe SimpleConstraint)
pickSimplifiable = do
[SimpleConstraint]
curCs <- forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' SimplifyState [SimpleConstraint]
ssConstraints
case forall a. (a -> Bool) -> [a] -> Maybe (a, [a])
pick SimpleConstraint -> Bool
simplifiable [SimpleConstraint]
curCs of
Maybe (SimpleConstraint, [SimpleConstraint])
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Just (SimpleConstraint
a, [SimpleConstraint]
as) -> do
Lens' SimplifyState [SimpleConstraint]
ssConstraints forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> a -> Sem r ()
.= [SimpleConstraint]
as
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just SimpleConstraint
a)
pick :: (a -> Bool) -> [a] -> Maybe (a, [a])
pick :: forall a. (a -> Bool) -> [a] -> Maybe (a, [a])
pick a -> Bool
_ [] = forall a. Maybe a
Nothing
pick a -> Bool
p (a
a : [a]
as)
| a -> Bool
p a
a = forall a. a -> Maybe a
Just (a
a, [a]
as)
| Bool
otherwise = forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (a
a forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> Maybe (a, [a])
pick a -> Bool
p [a]
as
simplifiable :: SimpleConstraint -> Bool
simplifiable :: SimpleConstraint -> Bool
simplifiable (Type
_ :=: Type
_) = Bool
True
simplifiable (TyCon {} :<: TyCon {}) = Bool
True
simplifiable (TyVar {} :<: TyCon {}) = Bool
True
simplifiable (TyCon {} :<: TyVar {}) = Bool
True
simplifiable (TyCon (CUser String
_) [Type]
_ :<: Type
_) = Bool
True
simplifiable (Type
_ :<: TyCon (CUser String
_) [Type]
_) = Bool
True
simplifiable (TyAtom (ABase BaseTy
_) :<: TyAtom (ABase BaseTy
_)) = Bool
True
simplifiable SimpleConstraint
_ = Bool
False
simplifyOne ::
Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r =>
SimpleConstraint ->
Sem r ()
simplifyOne :: forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
SimpleConstraint -> Sem r ()
simplifyOne SimpleConstraint
c = do
Set SimpleConstraint
seen <- forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' SimplifyState (Set SimpleConstraint)
ssSeen
case SimpleConstraint
c forall a. Ord a => a -> Set a -> Bool
`S.member` Set SimpleConstraint
seen of
Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Bool
False -> do
Lens' SimplifyState (Set SimpleConstraint)
ssSeen forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= forall a. Ord a => a -> Set a -> Set a
S.insert SimpleConstraint
c
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
SimpleConstraint -> Sem r ()
simplifyOne' SimpleConstraint
c
simplifyOne' ::
Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r =>
SimpleConstraint ->
Sem r ()
simplifyOne' :: forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
SimpleConstraint -> Sem r ()
simplifyOne' (Type
ty1 :=: Type
ty2) = do
TyDefCtx
tyDefns <- forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
case TyDefCtx -> [(Type, Type)] -> Maybe S
unify TyDefCtx
tyDefns [(Type
ty1, Type
ty2)] of
Maybe S
Nothing -> forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
Just S
s' -> forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
S -> Sem r ()
extendSubst S
s'
simplifyOne' (ty1 :: Type
ty1@(TyCon (CUser String
_) [Type]
_) :<: ty2 :: Type
ty2@TyVar {}) =
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
SimpleConstraint -> Sem r ()
simplifyOne' (Type
ty1 Type -> Type -> SimpleConstraint
:=: Type
ty2)
simplifyOne' (TyCon (CUser String
t) [Type]
ts :<: Type
ty2) = do
TyDefCtx
tyDefns <- forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
t TyDefCtx
tyDefns of
Maybe TyDefBody
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show String
t forall a. [a] -> [a] -> [a]
++ String
" not in ty defn map!"
Just (TyDefBody [String]
_ [Type] -> Type
body) ->
Lens' SimplifyState [SimpleConstraint]
ssConstraints forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= (([Type] -> Type
body [Type]
ts Type -> Type -> SimpleConstraint
:<: Type
ty2) forall a. a -> [a] -> [a]
:)
simplifyOne' (ty1 :: Type
ty1@TyVar {} :<: ty2 :: Type
ty2@(TyCon (CUser String
_) [Type]
_)) =
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
SimpleConstraint -> Sem r ()
simplifyOne' (Type
ty1 Type -> Type -> SimpleConstraint
:=: Type
ty2)
simplifyOne' (Type
ty1 :<: TyCon (CUser String
t) [Type]
ts) = do
TyDefCtx
tyDefns <- forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
t TyDefCtx
tyDefns of
Maybe TyDefBody
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show String
t forall a. [a] -> [a] -> [a]
++ String
" not in ty defn map!"
Just (TyDefBody [String]
_ [Type] -> Type
body) ->
Lens' SimplifyState [SimpleConstraint]
ssConstraints forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= ((Type
ty1 Type -> Type -> SimpleConstraint
:<: [Type] -> Type
body [Type]
ts) forall a. a -> [a] -> [a]
:)
simplifyOne' (TyCon c1 :: Con
c1@(CContainer Atom
ctr1) [Type]
tys1 :<: TyCon (CContainer Atom
ctr2) [Type]
tys2) =
Lens' SimplifyState [SimpleConstraint]
ssConstraints
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= ( ( (Atom -> Type
TyAtom Atom
ctr1 Type -> Type -> SimpleConstraint
:<: Atom -> Type
TyAtom Atom
ctr2)
forall a. a -> [a] -> [a]
: forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Variance -> Type -> Type -> SimpleConstraint
variance (Con -> [Variance]
arity Con
c1) [Type]
tys1 [Type]
tys2
)
forall a. [a] -> [a] -> [a]
++
)
simplifyOne' (TyCon Con
c1 [Type]
tys1 :<: TyCon Con
c2 [Type]
tys2)
| Con
c1 forall a. Eq a => a -> a -> Bool
/= Con
c2 = forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
| Bool
otherwise =
Lens' SimplifyState [SimpleConstraint]
ssConstraints forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= (forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Variance -> Type -> Type -> SimpleConstraint
variance (Con -> [Variance]
arity Con
c1) [Type]
tys1 [Type]
tys2 forall a. [a] -> [a] -> [a]
++)
simplifyOne' con :: SimpleConstraint
con@(TyVar Name Type
a :<: TyCon Con
c [Type]
_) = forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
Name Type -> Con -> SimpleConstraint -> Sem r ()
expandStruct Name Type
a Con
c SimpleConstraint
con
simplifyOne' con :: SimpleConstraint
con@(TyCon Con
c [Type]
_ :<: TyVar Name Type
a) = forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
Name Type -> Con -> SimpleConstraint -> Sem r ()
expandStruct Name Type
a Con
c SimpleConstraint
con
simplifyOne' (TyAtom (ABase BaseTy
b1) :<: TyAtom (ABase BaseTy
b2)) = do
case BaseTy -> BaseTy -> Bool
isSubB BaseTy
b1 BaseTy
b2 of
Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Bool
False -> forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
simplifyOne' (Type
s :<: Type
t) =
forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! simplifyOne' " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
s forall a. [a] -> [a] -> [a]
++ String
" :<: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
t
expandStruct ::
Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r =>
Name Type ->
Con ->
SimpleConstraint ->
Sem r ()
expandStruct :: forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
Name Type -> Con -> SimpleConstraint -> Sem r ()
expandStruct Name Type
a Con
c SimpleConstraint
con = do
[Type]
as <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const (Name Type -> Type
TyVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"a"))) (Con -> [Variance]
arity Con
c)
let s' :: S
s' = Name Type
a forall a. Name a -> a -> Substitution a
|-> Con -> [Type] -> Type
TyCon Con
c [Type]
as
Lens' SimplifyState [SimpleConstraint]
ssConstraints forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= (SimpleConstraint
con forall a. a -> [a] -> [a]
:)
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
S -> Sem r ()
extendSubst S
s'
extendSubst ::
Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r =>
S ->
Sem r ()
extendSubst :: forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
S -> Sem r ()
extendSubst S
s' = do
Lens' SimplifyState S
ssSubst forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= (S
s' forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@)
Lens' SimplifyState [SimpleConstraint]
ssConstraints forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= forall b a. Subst b a => Substitution b -> a -> a
applySubst S
s'
forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
S -> Sem r ()
substVarMap S
s'
substVarMap ::
Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r =>
S ->
Sem r ()
substVarMap :: forall (r :: [(* -> *) -> * -> *]).
Members
'[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
r =>
S -> Sem r ()
substVarMap S
s' = do
TyVarInfoMap
vm <- forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' SimplifyState TyVarInfoMap
ssVarMap
let tySorts :: [(Type, Sort)]
tySorts :: [(Type, Sort)]
tySorts = forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Lens' TyVarInfo Sort
tyVarSort)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Name Type -> TyVarInfoMap -> Maybe TyVarInfo
`lookupVM` TyVarInfoMap
vm) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> (b, a)
swap) forall a b. (a -> b) -> a -> b
$ forall a. Substitution a -> [(Name a, a)]
Subst.toList S
s'
tyQualList :: [(Type, Qualifier)]
tyQualList :: [(Type, Qualifier)]
tyQualList = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall a. Set a -> [a]
S.toList) [(Type, Sort)]
tySorts
TyVarInfoMap
vm' <- forall a. Monoid a => [a] -> a
mconcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Type -> Qualifier -> Sem r TyVarInfoMap
decomposeQual) [(Type, Qualifier)]
tyQualList
Lens' SimplifyState TyVarInfoMap
ssVarMap forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> a -> Sem r ()
.= TyVarInfoMap
vm' forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip Name Type -> TyVarInfoMap -> TyVarInfoMap
deleteVM) TyVarInfoMap
vm (forall a. Substitution a -> Set (Name a)
dom S
s')
variance :: Variance -> Type -> Type -> SimpleConstraint
variance Variance
Co Type
ty1 Type
ty2 = Type
ty1 Type -> Type -> SimpleConstraint
:<: Type
ty2
variance Variance
Contra Type
ty1 Type
ty2 = Type
ty2 Type -> Type -> SimpleConstraint
:<: Type
ty1
mkConstraintGraph :: (Show a, Ord a) => Set a -> [(a, a)] -> Graph a
mkConstraintGraph :: forall a. (Show a, Ord a) => Set a -> [(a, a)] -> Graph a
mkConstraintGraph Set a
as [(a, a)]
cs = forall a. (Show a, Ord a) => Set a -> Set (a, a) -> Graph a
G.mkGraph Set a
nodes (forall a. Ord a => [a] -> Set a
S.fromList [(a, a)]
cs)
where
nodes :: Set a
nodes = Set a
as forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. Ord a => [a] -> Set a
S.fromList ([(a, a)]
cs forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s t a b. Each s t a b => Traversal s t a b
each)
checkSkolems ::
Members '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
TyVarInfoMap ->
Graph Atom ->
Sem r (Graph UAtom, S)
checkSkolems :: forall ann (r :: [(* -> *) -> * -> *]).
Members
'[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
checkSkolems TyVarInfoMap
vm Graph Atom
graph = do
let skolemWCCs :: [Set Atom]
skolemWCCs :: [Set Atom]
skolemWCCs = forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Atom -> Bool
isSkolem) forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Graph a -> [Set a]
G.wcc Graph Atom
graph
ok :: Set Atom -> Bool
ok Set Atom
wcc =
forall a. Set a -> Int
S.size (forall a. (a -> Bool) -> Set a -> Set a
S.filter Atom -> Bool
isSkolem Set Atom
wcc) forall a. Ord a => a -> a -> Bool
<= Int
1
Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
( \case
ABase BaseTy
_ -> Bool
False
AVar (S Name Type
_) -> Bool
True
AVar (U Name Type
v) -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (forall a. Set a -> Bool
S.null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Lens' TyVarInfo Sort
tyVarSort) (Name Type -> TyVarInfoMap -> Maybe TyVarInfo
lookupVM Name Type
v TyVarInfoMap
vm)
)
Set Atom
wcc
([Set Atom]
good, [Set Atom]
bad) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Set Atom -> Bool
ok [Set Atom]
skolemWCCs
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Set Atom]
bad) forall a b. (a -> b) -> a -> b
$ forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
forall ann (r :: [(* -> *) -> * -> *]).
Members
'[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
graph forall a. Substitution a
idS [Set Atom]
good
where
noSkolems :: Atom -> UAtom
noSkolems :: Atom -> UAtom
noSkolems (ABase BaseTy
b) = BaseTy -> UAtom
UB BaseTy
b
noSkolems (AVar (U Name Type
v)) = Name Type -> UAtom
UV Name Type
v
noSkolems (AVar (S Name Type
v)) = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Skolem " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name Type
v forall a. [a] -> [a] -> [a]
++ String
" remaining in noSkolems"
unifyWCCs ::
Members '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
Graph Atom ->
S ->
[Set Atom] ->
Sem r (Graph UAtom, S)
unifyWCCs :: forall ann (r :: [(* -> *) -> * -> *]).
Members
'[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
g S
s [] = forall (m :: * -> *) a. Monad m => a -> m a
return (forall b a. Ord b => (a -> b) -> Graph a -> Graph b
G.map Atom -> UAtom
noSkolems Graph Atom
g, S
s)
unifyWCCs Graph Atom
g S
s (Set Atom
u : [Set Atom]
us) = do
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Unifying" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: [(* -> *) -> * -> *]) ann.
Pretty t =>
t -> Sem r (Doc ann)
pretty' (Set Atom
u forall a. a -> [a] -> [a]
: [Set Atom]
us) forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ann)
"..."
TyDefCtx
tyDefns <- forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
let g' :: Graph Atom
g' = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. (Show a, Ord a) => a -> Graph a -> Graph a
G.delete) Graph Atom
g Set Atom
u
ms' :: Maybe (Substitution Atom)
ms' = TyDefCtx -> [Atom] -> Maybe (Substitution Atom)
unifyAtoms TyDefCtx
tyDefns (forall a. Set a -> [a]
S.toList Set Atom
u)
case Maybe (Substitution Atom)
ms' of
Maybe (Substitution Atom)
Nothing -> forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
Just Substitution Atom
s' -> forall ann (r :: [(* -> *) -> * -> *]).
Members
'[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
g' (Substitution Atom -> S
atomToTypeSubst Substitution Atom
s' forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ S
s) [Set Atom]
us
elimCycles ::
Members '[Error SolveError] r =>
TyDefCtx ->
Graph UAtom ->
Sem r (Graph UAtom, S)
elimCycles :: forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError] r =>
TyDefCtx -> Graph UAtom -> Sem r (Graph UAtom, S)
elimCycles TyDefCtx
tyDefns = forall a b (r :: [(* -> *) -> * -> *]).
(Subst a a, Ord a, Members '[Error SolveError] r) =>
(Substitution a -> Substitution b)
-> ([a] -> Maybe (Substitution a))
-> Graph a
-> Sem r (Graph a, Substitution b)
elimCyclesGen Substitution UAtom -> S
uatomToTypeSubst (TyDefCtx -> [UAtom] -> Maybe (Substitution UAtom)
unifyUAtoms TyDefCtx
tyDefns)
elimCyclesGen ::
forall a b r.
(Subst a a, Ord a, Members '[Error SolveError] r) =>
(Substitution a -> Substitution b) ->
([a] -> Maybe (Substitution a)) ->
Graph a ->
Sem r (Graph a, Substitution b)
elimCyclesGen :: forall a b (r :: [(* -> *) -> * -> *]).
(Subst a a, Ord a, Members '[Error SolveError] r) =>
(Substitution a -> Substitution b)
-> ([a] -> Maybe (Substitution a))
-> Graph a
-> Sem r (Graph a, Substitution b)
elimCyclesGen Substitution a -> Substitution b
genSubst [a] -> Maybe (Substitution a)
genUnify Graph a
g =
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Maybe a -> Sem r a
note SolveError
NoUnify forall a b. (a -> b) -> a -> b
$
(forall b a. Ord b => (a -> b) -> Graph a -> Graph b
G.map forall a b. (a, b) -> a
fst forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (Substitution a -> Substitution b
genSubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (t :: * -> *).
(Subst a a, Foldable t) =>
t (Substitution a) -> Substitution a
compose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Graph a -> Set a
G.nodes)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Graph (a, Substitution a))
g'
where
g' :: Maybe (Graph (a, Substitution a))
g' :: Maybe (Graph (a, Substitution a))
g' = forall a. Ord a => Graph (Maybe a) -> Maybe (Graph a)
G.sequenceGraph forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> Graph a -> Graph b
G.map Set a -> Maybe (a, Substitution a)
unifySCC (forall a. Ord a => Graph a -> Graph (Set a)
G.condensation Graph a
g)
unifySCC :: Set a -> Maybe (a, Substitution a)
unifySCC :: Set a -> Maybe (a, Substitution a)
unifySCC Set a
uatoms = case forall a. Set a -> [a]
S.toList Set a
uatoms of
[] -> forall a. HasCallStack => String -> a
error String
"Impossible! unifySCC on the empty set"
as :: [a]
as@(a
a : [a]
_) -> (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall b a. Subst b a => Substitution b -> a -> a
applySubst a
a forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall a. a -> a
id) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Maybe (Substitution a)
genUnify [a]
as
isBaseEdge :: (UAtom, UAtom) -> Either (BaseTy, BaseTy) (UAtom, UAtom)
isBaseEdge :: (UAtom, UAtom) -> Either (BaseTy, BaseTy) (UAtom, UAtom)
isBaseEdge (UB BaseTy
b1, UB BaseTy
b2) = forall a b. a -> Either a b
Left (BaseTy
b1, BaseTy
b2)
isBaseEdge (UAtom, UAtom)
e = forall a b. b -> Either a b
Right (UAtom, UAtom)
e
checkBaseEdge :: Members '[Error SolveError] r => (BaseTy, BaseTy) -> Sem r ()
checkBaseEdge :: forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError] r =>
(BaseTy, BaseTy) -> Sem r ()
checkBaseEdge (BaseTy
b1, BaseTy
b2)
| BaseTy -> BaseTy -> Bool
isSubB BaseTy
b1 BaseTy
b2 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise = forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
checkBaseEdges :: Members '[Error SolveError] r => Graph UAtom -> Sem r (Graph UAtom)
checkBaseEdges :: forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError] r =>
Graph UAtom -> Sem r (Graph UAtom)
checkBaseEdges Graph UAtom
g = do
let ([(BaseTy, BaseTy)]
baseEdges, [(UAtom, UAtom)]
varEdges) = forall a b. [Either a b] -> ([a], [b])
partitionEithers forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (UAtom, UAtom) -> Either (BaseTy, BaseTy) (UAtom, UAtom)
isBaseEdge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => Graph a -> Set (a, a)
G.edges forall a b. (a -> b) -> a -> b
$ Graph UAtom
g
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError] r =>
(BaseTy, BaseTy) -> Sem r ()
checkBaseEdge [(BaseTy, BaseTy)]
baseEdges
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (Show a, Ord a) => Set a -> Set (a, a) -> Graph a
G.mkGraph (forall a. Graph a -> Set a
G.nodes Graph UAtom
g) (forall a. Ord a => [a] -> Set a
S.fromList [(UAtom, UAtom)]
varEdges)
data Rels = Rels
{ Rels -> Set BaseTy
baseRels :: Set BaseTy
, Rels -> Set (Name Type)
varRels :: Set (Name Type)
}
deriving (Int -> Rels -> ShowS
[Rels] -> ShowS
Rels -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Rels] -> ShowS
$cshowList :: [Rels] -> ShowS
show :: Rels -> String
$cshow :: Rels -> String
showsPrec :: Int -> Rels -> ShowS
$cshowsPrec :: Int -> Rels -> ShowS
Show, Rels -> Rels -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rels -> Rels -> Bool
$c/= :: Rels -> Rels -> Bool
== :: Rels -> Rels -> Bool
$c== :: Rels -> Rels -> Bool
Eq)
newtype RelMap = RelMap {RelMap -> Map (Name Type, Dir) Rels
unRelMap :: Map (Name Type, Dir) Rels}
instance Pretty RelMap where
pretty :: forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
RelMap -> Sem r (Doc ann)
pretty (RelMap Map (Name Type, Dir) Rels
rm) = forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall {r :: [(* -> *) -> * -> *]} {t} {ann}.
(Member (Reader PA) r, Member LFresh r, Pretty t) =>
(Rels, t, Rels) -> Sem r (Doc ann)
prettyVar [(Rels, Name Type, Rels)]
byVar)
where
vars :: Set (Name Type)
vars = forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map forall a b. (a, b) -> a
fst (forall k a. Map k a -> Set k
M.keysSet Map (Name Type, Dir) Rels
rm)
byVar :: [(Rels, Name Type, Rels)]
byVar = forall a b. (a -> b) -> [a] -> [b]
map (\Name Type
x -> (Map (Name Type, Dir) Rels
rm forall k a. Ord k => Map k a -> k -> a
! (Name Type
x, Dir
SubTy), Name Type
x, Map (Name Type, Dir) Rels
rm forall k a. Ord k => Map k a -> k -> a
! (Name Type
x, Dir
SuperTy))) (forall a. Set a -> [a]
S.toList Set (Name Type)
vars)
prettyVar :: (Rels, t, Rels) -> Sem r (Doc ann)
prettyVar (Rels
subs, t
x, Rels
sups) = forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [forall {r :: [(* -> *) -> * -> *]} {ann}.
(Member (Reader PA) r, Member LFresh r) =>
Rels -> Sem r (Doc ann)
prettyRel Rels
subs, Sem r (Doc ann)
"<:", forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty t
x, Sem r (Doc ann)
"<:", forall {r :: [(* -> *) -> * -> *]} {ann}.
(Member (Reader PA) r, Member LFresh r) =>
Rels -> Sem r (Doc ann)
prettyRel Rels
sups]
prettyRel :: Rels -> Sem r (Doc ann)
prettyRel Rels
rs = forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty (Rels -> Set BaseTy
baseRels Rels
rs) forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ann)
", " forall a. Semigroup a => a -> a -> a
<> forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty (Rels -> Set (Name Type)
varRels Rels
rs)
substRel :: Name Type -> BaseTy -> RelMap -> RelMap
substRel :: Name Type -> BaseTy -> RelMap -> RelMap
substRel Name Type
x BaseTy
ty =
Map (Name Type, Dir) Rels -> RelMap
RelMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Map k a
M.delete (Name Type
x, Dir
SuperTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Map k a
M.delete (Name Type
x, Dir
SubTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b k. (a -> b) -> Map k a -> Map k b
M.map (\r :: Rels
r@(Rels Set BaseTy
b Set (Name Type)
v) -> if Name Type
x forall a. Ord a => a -> Set a -> Bool
`S.member` Set (Name Type)
v then Set BaseTy -> Set (Name Type) -> Rels
Rels (forall a. Ord a => a -> Set a -> Set a
S.insert BaseTy
ty Set BaseTy
b) (forall a. Ord a => a -> Set a -> Set a
S.delete Name Type
x Set (Name Type)
v) else Rels
r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelMap -> Map (Name Type, Dir) Rels
unRelMap
dirtypesBySort :: TyVarInfoMap -> RelMap -> Dir -> BaseTy -> Sort -> Set (Name Type) -> [BaseTy]
dirtypesBySort :: TyVarInfoMap
-> RelMap -> Dir -> BaseTy -> Sort -> Set (Name Type) -> [BaseTy]
dirtypesBySort TyVarInfoMap
vm (RelMap Map (Name Type, Dir) Rels
relMap) Dir
dir BaseTy
t Sort
s Set (Name Type)
x =
forall {a}. [a] -> (a -> Bool) -> [a]
keep (Dir -> BaseTy -> [BaseTy]
dirtypes Dir
dir BaseTy
t) forall a b. (a -> b) -> a -> b
$ \BaseTy
t' ->
BaseTy -> Sort -> Bool
hasSort BaseTy
t' Sort
s
Bool -> Bool -> Bool
&&
forall (t :: * -> *) a. Foldable t => t a -> (a -> Bool) -> Bool
forAll
Set (Name Type)
x
( \Name Type
beta ->
forall (t :: * -> *) a. Foldable t => t a -> (a -> Bool) -> Bool
exists (Dir -> BaseTy -> [BaseTy]
dirtypes (Dir -> Dir
other Dir
dir) BaseTy
t') forall a b. (a -> b) -> a -> b
$ \BaseTy
t'' ->
BaseTy -> Sort -> Bool
hasSort BaseTy
t'' (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
beta)
Bool -> Bool -> Bool
&&
forall (t :: * -> *) a. Foldable t => t a -> (a -> Bool) -> Bool
forAll
(Rels -> Set BaseTy
baseRels (forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"dirtypesBySort, beta rel" Map (Name Type, Dir) Rels
relMap (Name Type
beta, Dir -> Dir
other Dir
dir)))
(Dir -> BaseTy -> BaseTy -> Bool
isDirB Dir
dir BaseTy
t'')
)
where
forAll, exists :: Foldable t => t a -> (a -> Bool) -> Bool
forAll :: forall (t :: * -> *) a. Foldable t => t a -> (a -> Bool) -> Bool
forAll = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
exists :: forall (t :: * -> *) a. Foldable t => t a -> (a -> Bool) -> Bool
exists = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any
keep :: [a] -> (a -> Bool) -> [a]
keep = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. (a -> Bool) -> [a] -> [a]
filter
limBySort :: TyVarInfoMap -> RelMap -> Dir -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
limBySort :: TyVarInfoMap
-> RelMap
-> Dir
-> [BaseTy]
-> Sort
-> Set (Name Type)
-> Maybe BaseTy
limBySort TyVarInfoMap
vm RelMap
rm Dir
dir [BaseTy]
ts Sort
s Set (Name Type)
x =
(\[BaseTy]
is -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\BaseTy
lim -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\BaseTy
u -> Dir -> BaseTy -> BaseTy -> Bool
isDirB Dir
dir BaseTy
u BaseTy
lim) [BaseTy]
is) [BaseTy]
is)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[BaseTy]] -> [BaseTy]
isects
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\BaseTy
t -> TyVarInfoMap
-> RelMap -> Dir -> BaseTy -> Sort -> Set (Name Type) -> [BaseTy]
dirtypesBySort TyVarInfoMap
vm RelMap
rm Dir
dir BaseTy
t Sort
s Set (Name Type)
x)
forall a b. (a -> b) -> a -> b
$ [BaseTy]
ts
where
isects :: [[BaseTy]] -> [BaseTy]
isects = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 forall a. Eq a => [a] -> [a] -> [a]
intersect
lubBySort, glbBySort :: TyVarInfoMap -> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort :: TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort TyVarInfoMap
vm RelMap
rm = TyVarInfoMap
-> RelMap
-> Dir
-> [BaseTy]
-> Sort
-> Set (Name Type)
-> Maybe BaseTy
limBySort TyVarInfoMap
vm RelMap
rm Dir
SuperTy
glbBySort :: TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
glbBySort TyVarInfoMap
vm RelMap
rm = TyVarInfoMap
-> RelMap
-> Dir
-> [BaseTy]
-> Sort
-> Set (Name Type)
-> Maybe BaseTy
limBySort TyVarInfoMap
vm RelMap
rm Dir
SubTy
solveGraph ::
Members '[Fresh, Error SolveError, Output (Message ann)] r =>
TyVarInfoMap ->
Graph UAtom ->
Sem r S
solveGraph :: forall ann (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output (Message ann)] r =>
TyVarInfoMap -> Graph UAtom -> Sem r S
solveGraph TyVarInfoMap
vm Graph UAtom
g = Substitution Atom -> S
atomToTypeSubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution BaseTy -> Substitution Atom
unifyWCC forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ann (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output (Message ann)] r =>
RelMap -> Sem r (Substitution BaseTy)
go RelMap
topRelMap
where
unifyWCC :: Substitution BaseTy -> Substitution Atom
unifyWCC :: Substitution BaseTy -> Substitution Atom
unifyWCC Substitution BaseTy
s = forall a (t :: * -> *).
(Subst a a, Foldable t) =>
t (Substitution a) -> Substitution a
compose (forall a b. (a -> b) -> [a] -> [b]
map Set (Name Type) -> Substitution Atom
mkEquateSubst [Set (Name Type)]
wccVarGroups) forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BaseTy -> Atom
ABase Substitution BaseTy
s
where
wccVarGroups :: [Set (Name Type)]
wccVarGroups :: [Set (Name Type)]
wccVarGroups = forall a b. (a -> b) -> [a] -> [b]
map (forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map UAtom -> Name Type
getVar) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all UAtom -> Bool
uisVar) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Subst b a => Substitution b -> a -> a
applySubst Substitution BaseTy
s forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Graph a -> [Set a]
G.wcc Graph UAtom
g
getVar :: UAtom -> Name Type
getVar (UV Name Type
v) = Name Type
v
getVar (UB BaseTy
b) =
forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
String
"Impossible! Base type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BaseTy
b forall a. [a] -> [a] -> [a]
++ String
" in solveGraph.getVar"
mkEquateSubst :: Set (Name Type) -> Substitution Atom
mkEquateSubst :: Set (Name Type) -> Substitution Atom
mkEquateSubst = [Name Type] -> Substitution Atom
mkEquations forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
S.toList
mkEquations :: [Name Type] -> Substitution Atom
mkEquations (Name Type
a : [Name Type]
as) = forall a. [(Name a, a)] -> Substitution a
Subst.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\Name Type
v -> (coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
v, Var -> Atom
AVar (Name Type -> Var
U Name Type
a))) forall a b. (a -> b) -> a -> b
$ [Name Type]
as
mkEquations [] = forall a. HasCallStack => String -> a
error String
"Impossible! Empty set of names in mkEquateSubst"
topRelMap :: RelMap
topRelMap :: RelMap
topRelMap =
Map (Name Type, Dir) Rels -> RelMap
RelMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b k. (a -> b) -> Map k a -> Map k b
M.map
( forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Set BaseTy -> Set (Name Type) -> Rels
Rels
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Eq a => [a] -> Set a
S.fromAscList forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. Eq a => [a] -> Set a
S.fromAscList)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [Either a b] -> ([a], [b])
partitionEithers
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map UAtom -> Either BaseTy (Name Type)
uatomToEither
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
S.toList
)
forall a b. (a -> b) -> a -> b
$ forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys (,Dir
SuperTy) Map (Name Type) (Set UAtom)
subMap forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys (,Dir
SubTy) Map (Name Type) (Set UAtom)
superMap
subMap, superMap :: Map (Name Type) (Set UAtom)
(Map (Name Type) (Set UAtom)
subMap, Map (Name Type) (Set UAtom)
superMap) = (Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom)
onlyVars forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom)
onlyVars) forall a b. (a -> b) -> a -> b
$ forall a.
(Show a, Ord a) =>
Graph a -> (Map a (Set a), Map a (Set a))
G.cessors Graph UAtom
g
onlyVars :: Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom)
onlyVars :: Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom)
onlyVars = forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys UAtom -> Name Type
fromVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey (\UAtom
a Set UAtom
_ -> UAtom -> Bool
uisVar UAtom
a)
where
fromVar :: UAtom -> Name Type
fromVar (UV Name Type
x) = Name Type
x
fromVar UAtom
_ = forall a. HasCallStack => String -> a
error String
"Impossible! UB but uisVar."
go ::
Members '[Fresh, Error SolveError, Output (Message ann)] r =>
RelMap ->
Sem r (Substitution BaseTy)
go :: forall ann (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output (Message ann)] r =>
RelMap -> Sem r (Substitution BaseTy)
go relMap :: RelMap
relMap@(RelMap Map (Name Type, Dir) Rels
rm) =
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty RelMap
relMap forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> case [Name Type]
as of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Substitution a
idS
(Name Type
a : [Name Type]
_) -> do
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Solving for" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: [(* -> *) -> * -> *]) ann.
Pretty t =>
t -> Sem r (Doc ann)
pretty' Name Type
a
case Name Type -> Maybe (Substitution BaseTy)
solveVar Name Type
a of
Maybe (Substitution BaseTy)
Nothing -> do
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Couldn't solve for" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: [(* -> *) -> * -> *]) ann.
Pretty t =>
t -> Sem r (Doc ann)
pretty' Name Type
a
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
Just Substitution BaseTy
s -> do
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty Substitution BaseTy
s
(forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ Substitution BaseTy
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ann (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output (Message ann)] r =>
RelMap -> Sem r (Substitution BaseTy)
go (Name Type -> BaseTy -> RelMap -> RelMap
substRel Name Type
a (forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall a. Name a -> Substitution a -> Maybe a
Subst.lookup (coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
a) Substitution BaseTy
s) RelMap
relMap)
where
asBase :: [Name Type]
asBase =
forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> Bool
S.null forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rels -> Set BaseTy
baseRels forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveGraph.go.as" Map (Name Type, Dir) Rels
rm)
forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys Map (Name Type, Dir) Rels
rm
as :: [Name Type]
as = case [Name Type]
asBase of
[] -> forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
/= Sort
topSort) forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys Map (Name Type, Dir) Rels
rm
[Name Type]
_ -> [Name Type]
asBase
solveVar :: Name Type -> Maybe (Substitution BaseTy)
solveVar :: Name Type -> Maybe (Substitution BaseTy)
solveVar Name Type
v =
case ((Name Type
v, Dir
SuperTy), (Name Type
v, Dir
SubTy)) forall a b. a -> (a -> b) -> b
& forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over forall (r :: * -> * -> *) a b.
Bitraversable r =>
Traversal (r a a) (r b b) a b
both (forall a. Set a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rels -> Set BaseTy
baseRels forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveGraph.solveVar" Map (Name Type, Dir) Rels
rm) of
([], []) ->
if TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
S.fromList [Qualifier
QBool]
then forall a. a -> Maybe a
Just (coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
v forall a. Name a -> a -> Substitution a
|-> BaseTy
B)
else
(coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
v forall a. Name a -> a -> Substitution a
|->)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort
TyVarInfoMap
vm
RelMap
relMap
[BaseTy
N]
(TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
(Rels -> Set (Name Type)
varRels (forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveVar none, rels" Map (Name Type, Dir) Rels
rm (Name Type
v, Dir
SubTy)))
([BaseTy]
bsupers, []) ->
(coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
v forall a. Name a -> a -> Substitution a
|->)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
glbBySort
TyVarInfoMap
vm
RelMap
relMap
[BaseTy]
bsupers
(TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
(Rels -> Set (Name Type)
varRels (forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveVar bsupers, rels" Map (Name Type, Dir) Rels
rm (Name Type
v, Dir
SuperTy)))
([], [BaseTy]
bsubs) ->
(coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
v forall a. Name a -> a -> Substitution a
|->)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort
TyVarInfoMap
vm
RelMap
relMap
[BaseTy]
bsubs
(TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
(Rels -> Set (Name Type)
varRels (forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveVar bsubs, rels" Map (Name Type, Dir) Rels
rm (Name Type
v, Dir
SubTy)))
([BaseTy]
bsupers, [BaseTy]
bsubs) -> do
BaseTy
ub <-
TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
glbBySort
TyVarInfoMap
vm
RelMap
relMap
[BaseTy]
bsupers
(TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
(Rels -> Set (Name Type)
varRels (Map (Name Type, Dir) Rels
rm forall k a. Ord k => Map k a -> k -> a
! (Name Type
v, Dir
SuperTy)))
BaseTy
lb <-
TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort
TyVarInfoMap
vm
RelMap
relMap
[BaseTy]
bsubs
(TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
(Rels -> Set (Name Type)
varRels (Map (Name Type, Dir) Rels
rm forall k a. Ord k => Map k a -> k -> a
! (Name Type
v, Dir
SubTy)))
case BaseTy -> BaseTy -> Bool
isSubB BaseTy
lb BaseTy
ub of
Bool
True -> forall a. a -> Maybe a
Just (coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
v forall a. Name a -> a -> Substitution a
|-> BaseTy
lb)
Bool
False -> forall a. Maybe a
Nothing