{-# LANGUAGE DeriveAnyClass    #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell   #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Disco.Typecheck.Solve
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Constraint solver for the constraints generated during type
-- checking/inference.
-----------------------------------------------------------------------------

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

--------------------------------------------------
-- Solver errors

-- | Type of errors which can be generated by the constraint solving
--   process.
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
(Int -> SolveError -> ShowS)
-> (SolveError -> String)
-> ([SolveError] -> ShowS)
-> Show SolveError
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

--------------------------------------------------
-- Error utilities

runSolve :: Sem (Fresh ': Error SolveError ': r) a -> Sem r (Either SolveError a)
runSolve :: Sem (Fresh : Error SolveError : r) a -> Sem r (Either SolveError a)
runSolve = Sem (Error SolveError : r) a -> Sem r (Either SolveError a)
forall e (r :: [(* -> *) -> * -> *]) a.
Sem (Error e : r) a -> Sem r (Either e a)
runError (Sem (Error SolveError : r) a -> Sem r (Either SolveError a))
-> (Sem (Fresh : Error SolveError : r) a
    -> Sem (Error SolveError : r) a)
-> Sem (Fresh : Error SolveError : r) a
-> Sem r (Either SolveError a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem (Fresh : Error SolveError : r) a
-> Sem (Error SolveError : r) a
forall (r :: [(* -> *) -> * -> *]) a. Sem (Fresh : r) a -> Sem r a
runFresh

-- | Run a list of actions, and return the results from those which do
--   not throw an error.  If all of them throw an error, rethrow the
--   first one.
filterErrors :: Member (Error e) r => [Sem r a] -> Sem r [a]
filterErrors :: [Sem r a] -> Sem r [a]
filterErrors [Sem r a]
ms = do
  [Either e a]
es <- (Sem r a -> Sem r (Either e a)) -> [Sem r a] -> Sem r [Either e a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Sem r a -> Sem r (Either e a)
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
Sem r a -> Sem r (Either e a)
try [Sem r a]
ms
  case [Either e a] -> ([e], [a])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either e a]
es of
    (e
e:[e]
_, []) -> e -> Sem r [a]
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw e
e
    ([e]
_, [a]
as)   -> [a] -> Sem r [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
as

-- | A variant of 'asum' which picks the first action that succeeds,
--   or re-throws the error of the last one if none of them
--   do. Precondition: the list must not be empty.
asum' :: Member (Error e) r => [Sem r a] -> Sem r a
asum' :: [Sem r a] -> Sem r a
asum' []     = String -> Sem r a
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 Sem r a -> (e -> Sem r a) -> Sem r a
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
Sem r a -> (e -> Sem r a) -> Sem r a
`catch` (\e
_ -> [Sem r a] -> Sem r a
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
[Sem r a] -> Sem r a
asum' [Sem r a]
ms)

--------------------------------------------------
-- Simple constraints

data SimpleConstraint where
  (:<:) :: Type -> Type -> SimpleConstraint
  (:=:) :: Type -> Type -> SimpleConstraint
  deriving (Int -> SimpleConstraint -> ShowS
[SimpleConstraint] -> ShowS
SimpleConstraint -> String
(Int -> SimpleConstraint -> ShowS)
-> (SimpleConstraint -> String)
-> ([SimpleConstraint] -> ShowS)
-> Show SimpleConstraint
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
(SimpleConstraint -> SimpleConstraint -> Bool)
-> (SimpleConstraint -> SimpleConstraint -> Bool)
-> Eq SimpleConstraint
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
Eq SimpleConstraint
-> (SimpleConstraint -> SimpleConstraint -> Ordering)
-> (SimpleConstraint -> SimpleConstraint -> Bool)
-> (SimpleConstraint -> SimpleConstraint -> Bool)
-> (SimpleConstraint -> SimpleConstraint -> Bool)
-> (SimpleConstraint -> SimpleConstraint -> Bool)
-> (SimpleConstraint -> SimpleConstraint -> SimpleConstraint)
-> (SimpleConstraint -> SimpleConstraint -> SimpleConstraint)
-> Ord 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
$cp1Ord :: Eq SimpleConstraint
Ord, (forall x. SimpleConstraint -> Rep SimpleConstraint x)
-> (forall x. Rep SimpleConstraint x -> SimpleConstraint)
-> Generic SimpleConstraint
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
Show SimpleConstraint
-> (AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx
    -> (AnyName -> f AnyName)
    -> SimpleConstraint
    -> f SimpleConstraint)
-> (AlphaCtx
    -> NamePatFind -> SimpleConstraint -> SimpleConstraint)
-> (AlphaCtx -> NthPatFind -> SimpleConstraint -> SimpleConstraint)
-> (SimpleConstraint -> DisjointSet AnyName)
-> (SimpleConstraint -> All)
-> (SimpleConstraint -> Bool)
-> (SimpleConstraint -> NthPatFind)
-> (SimpleConstraint -> NamePatFind)
-> (AlphaCtx
    -> Perm AnyName -> SimpleConstraint -> SimpleConstraint)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx
    -> SimpleConstraint
    -> (SimpleConstraint -> Perm AnyName -> m b)
    -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> SimpleConstraint -> m (SimpleConstraint, Perm AnyName))
-> (AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Ordering)
-> Alpha 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' :: AlphaCtx -> SimpleConstraint -> m (SimpleConstraint, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> SimpleConstraint -> m (SimpleConstraint, Perm AnyName)
lfreshen' :: 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' :: 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
$cp1Alpha :: Show SimpleConstraint
Alpha, Subst Type)

instance Pretty SimpleConstraint where
  pretty :: SimpleConstraint -> Sem r Doc
pretty = \case
    Type
ty1 :<: Type
ty2 -> Type -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty1 Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"<:" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Type -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty2
    Type
ty1 :=: Type
ty2 -> Type -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty1 Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"=" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Type -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty2

--------------------------------------------------
-- Simplifier types

-- Uses TH to generate lenses so it has to go here before other stuff.

---------------------------------
-- Variable maps

-- | Information about a particular type variable.  More information
--   may be added in the future (e.g. polarity).
data TyVarInfo = TVI
  { TyVarInfo -> First Ilk
_tyVarIlk  :: First Ilk   -- ^ The ilk (unification or skolem) of the variable, if known
  , TyVarInfo -> Sort
_tyVarSort :: Sort        -- ^ The sort (set of qualifiers) of the type variable.
  }
  deriving (Int -> TyVarInfo -> ShowS
[TyVarInfo] -> ShowS
TyVarInfo -> String
(Int -> TyVarInfo -> ShowS)
-> (TyVarInfo -> String)
-> ([TyVarInfo] -> ShowS)
-> Show TyVarInfo
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 :: TyVarInfo -> Sem r Doc
pretty (TVI (First Maybe Ilk
ilk) Sort
s) = Sem r Doc -> (Ilk -> Sem r Doc) -> Maybe Ilk -> Sem r Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Doc -> Sem r Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
"?") Ilk -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Maybe Ilk
ilk Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc
"%" Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sort -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Sort
s

-- | Create a 'TyVarInfo' given an 'Ilk' and a 'Sort'.
mkTVI :: Ilk -> Sort -> TyVarInfo
mkTVI :: Ilk -> Sort -> TyVarInfo
mkTVI = First Ilk -> Sort -> TyVarInfo
TVI (First Ilk -> Sort -> TyVarInfo)
-> (Ilk -> First Ilk) -> Ilk -> Sort -> TyVarInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Ilk -> First Ilk
forall a. Maybe a -> First a
First (Maybe Ilk -> First Ilk) -> (Ilk -> Maybe Ilk) -> Ilk -> First Ilk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ilk -> Maybe Ilk
forall a. a -> Maybe a
Just

-- | We can learn different things about a type variable from
--   different places; the 'Semigroup' instance allows combining
--   information about a type variable into a single record.
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 First Ilk -> First Ilk -> First Ilk
forall a. Semigroup a => a -> a -> a
<> First Ilk
i2) (Sort
s1 Sort -> Sort -> Sort
forall a. Semigroup a => a -> a -> a
<> Sort
s2)

-- | A 'TyVarInfoMap' records what we know about each type variable;
--   it is a mapping from type variable names to 'TyVarInfo' records.
newtype TyVarInfoMap = VM { TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM :: Map (Name Type) TyVarInfo }
  deriving (Int -> TyVarInfoMap -> ShowS
[TyVarInfoMap] -> ShowS
TyVarInfoMap -> String
(Int -> TyVarInfoMap -> ShowS)
-> (TyVarInfoMap -> String)
-> ([TyVarInfoMap] -> ShowS)
-> Show TyVarInfoMap
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 :: TyVarInfoMap -> Sem r Doc
pretty (VM Map (Name Type) TyVarInfo
m) = Map (Name Type) TyVarInfo -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Map (Name Type) TyVarInfo
m

-- | Utility function for acting on a 'TyVarInfoMap' by acting on the
--   underlying 'Map'.
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)

-- | Look up a given variable name in a 'TyVarInfoMap'.
lookupVM :: Name Type -> TyVarInfoMap -> Maybe TyVarInfo
lookupVM :: Name Type -> TyVarInfoMap -> Maybe TyVarInfo
lookupVM Name Type
v = Name Type -> Map (Name Type) TyVarInfo -> Maybe TyVarInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name Type
v (Map (Name Type) TyVarInfo -> Maybe TyVarInfo)
-> (TyVarInfoMap -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap
-> Maybe TyVarInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM

-- | Remove the mapping for a particular variable name (if it exists)
--   from a 'TyVarInfoMap'.
deleteVM :: Name Type -> TyVarInfoMap -> TyVarInfoMap
deleteVM :: Name Type -> TyVarInfoMap -> TyVarInfoMap
deleteVM = (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap -> TyVarInfoMap
onVM ((Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
 -> TyVarInfoMap -> TyVarInfoMap)
-> (Name Type
    -> Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> Name Type
-> TyVarInfoMap
-> TyVarInfoMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name Type -> Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo
forall k a. Ord k => k -> Map k a -> Map k a
M.delete

-- | Given a list of type variable names, add them all to the
--   'TyVarInfoMap' as 'Skolem' variables (with a trivial sort).
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 ((Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
 -> TyVarInfoMap -> TyVarInfoMap)
-> (Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap
-> TyVarInfoMap
forall a b. (a -> b) -> a -> b
$ \Map (Name Type) TyVarInfo
vm -> (Map (Name Type) TyVarInfo
 -> Name Type -> Map (Name Type) TyVarInfo)
-> Map (Name Type) TyVarInfo
-> [Name Type]
-> Map (Name Type) TyVarInfo
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Name Type
 -> Map (Name Type) TyVarInfo -> Map (Name Type) TyVarInfo)
-> Map (Name Type) TyVarInfo
-> Name Type
-> Map (Name Type) TyVarInfo
forall a b c. (a -> b -> c) -> b -> a -> c
flip (\Name Type
v -> Name Type
-> TyVarInfo
-> Map (Name Type) TyVarInfo
-> Map (Name Type) TyVarInfo
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name Type
v (Ilk -> Sort -> TyVarInfo
mkTVI Ilk
Skolem Sort
forall a. Monoid a => a
mempty))) Map (Name Type) TyVarInfo
vm [Name Type]
vs

-- | The @Semigroup@ instance for 'TyVarInfoMap' unions the two maps,
--   combining the info records for any variables occurring in both
--   maps.
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 ((TyVarInfo -> TyVarInfo -> TyVarInfo)
-> Map (Name Type) TyVarInfo
-> Map (Name Type) TyVarInfo
-> Map (Name Type) TyVarInfo
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith TyVarInfo -> TyVarInfo -> TyVarInfo
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 Map (Name Type) TyVarInfo
forall k a. Map k a
M.empty
  mappend :: TyVarInfoMap -> TyVarInfoMap -> TyVarInfoMap
mappend = TyVarInfoMap -> TyVarInfoMap -> TyVarInfoMap
forall a. Semigroup a => a -> a -> a
(<>)

-- | Get the sort of a particular variable recorded in a
--   'TyVarInfoMap'.  Returns the trivial (empty) sort for a variable
--   not in the map.
getSort :: TyVarInfoMap -> Name Type -> Sort
getSort :: TyVarInfoMap -> Name Type -> Sort
getSort (VM Map (Name Type) TyVarInfo
m) Name Type
v = Sort -> (TyVarInfo -> Sort) -> Maybe TyVarInfo -> Sort
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sort
topSort (Getting Sort TyVarInfo Sort -> TyVarInfo -> Sort
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Sort TyVarInfo Sort
Lens' TyVarInfo Sort
tyVarSort) (Name Type -> Map (Name Type) TyVarInfo -> Maybe TyVarInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name Type
v Map (Name Type) TyVarInfo
m)

-- | Get the 'Ilk' of a variable recorded in a 'TyVarInfoMap'.
--   Returns @Nothing@ if the variable is not in the map, or if its
--   ilk is not known.
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 Map (Name Type) TyVarInfo
-> Getting
     (First (First Ilk)) (Map (Name Type) TyVarInfo) (First Ilk)
-> Maybe (First Ilk)
forall s a. s -> Getting (First a) s a -> Maybe a
^? Index (Map (Name Type) TyVarInfo)
-> Traversal'
     (Map (Name Type) TyVarInfo) (IxValue (Map (Name Type) TyVarInfo))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (Map (Name Type) TyVarInfo)
Name Type
v ((TyVarInfo -> Const (First (First Ilk)) TyVarInfo)
 -> Map (Name Type) TyVarInfo
 -> Const (First (First Ilk)) (Map (Name Type) TyVarInfo))
-> ((First Ilk -> Const (First (First Ilk)) (First Ilk))
    -> TyVarInfo -> Const (First (First Ilk)) TyVarInfo)
-> Getting
     (First (First Ilk)) (Map (Name Type) TyVarInfo) (First Ilk)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (First Ilk -> Const (First (First Ilk)) (First Ilk))
-> TyVarInfo -> Const (First (First Ilk)) TyVarInfo
Lens' TyVarInfo (First Ilk)
tyVarIlk) Maybe (First Ilk) -> (First Ilk -> Maybe Ilk) -> Maybe Ilk
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= First Ilk -> Maybe Ilk
forall a. First a -> Maybe a
getFirst

-- | Extend the sort of a type variable by combining its existing sort
--   with the given one.  Has no effect if the variable is not already
--   in the map.
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 (Index (Map (Name Type) TyVarInfo)
-> Lens'
     (Map (Name Type) TyVarInfo)
     (Maybe (IxValue (Map (Name Type) TyVarInfo)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index (Map (Name Type) TyVarInfo)
Name Type
x ((Maybe TyVarInfo -> Identity (Maybe TyVarInfo))
 -> Map (Name Type) TyVarInfo
 -> Identity (Map (Name Type) TyVarInfo))
-> ((Sort -> Identity Sort)
    -> Maybe TyVarInfo -> Identity (Maybe TyVarInfo))
-> (Sort -> Identity Sort)
-> Map (Name Type) TyVarInfo
-> Identity (Map (Name Type) TyVarInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVarInfo -> Identity TyVarInfo)
-> Maybe TyVarInfo -> Identity (Maybe TyVarInfo)
forall a b. Prism (Maybe a) (Maybe b) a b
_Just ((TyVarInfo -> Identity TyVarInfo)
 -> Maybe TyVarInfo -> Identity (Maybe TyVarInfo))
-> ((Sort -> Identity Sort) -> TyVarInfo -> Identity TyVarInfo)
-> (Sort -> Identity Sort)
-> Maybe TyVarInfo
-> Identity (Maybe TyVarInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort -> Identity Sort) -> TyVarInfo -> Identity TyVarInfo
Lens' TyVarInfo Sort
tyVarSort ((Sort -> Identity Sort)
 -> Map (Name Type) TyVarInfo
 -> Identity (Map (Name Type) TyVarInfo))
-> (Sort -> Sort)
-> Map (Name Type) TyVarInfo
-> Map (Name Type) TyVarInfo
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Sort -> Sort -> Sort
forall a. Ord a => Set a -> Set a -> Set a
`S.union` Sort
s))

---------------------------------
-- Simplifier state

-- The simplification stage maintains a mutable state consisting of
-- the current qualifier map (containing wanted qualifiers for type
-- variables), the list of remaining SimpleConstraints, and the
-- current substitution.  It also keeps track of seen constraints, so
-- expansion of recursive types can stop when encountering a
-- previously seen constraint.
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 :: String -> Map k a -> k -> a
lkup String
messg Map k a
m k
k = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe (String -> a
forall a. HasCallStack => String -> a
error String
errMsg) (k -> Map k a -> Maybe a
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 = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ k -> String
forall a. Show a => a -> String
show k
k
      , String
"  Map = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Map k a -> String
forall a. Show a => a -> String
show Map k a
m
      , String
"  Location: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
messg
      ]

--------------------------------------------------
-- Top-level solver algorithm

solveConstraint
  :: Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r
  => Constraint -> Sem r S
solveConstraint :: Constraint -> Sem r S
solveConstraint Constraint
c = do

  -- Step 1. Open foralls (instantiating with skolem variables) and
  -- collect wanted qualifiers; also expand disjunctions.  Result in a
  -- list of possible constraint sets; each one consists of equational
  -- and subtyping constraints in addition to qualifiers.

  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Solving:"
  Constraint -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty Constraint
c

  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"------------------------------"
  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Decomposing constraints..."

  [(TyVarInfoMap, [SimpleConstraint])]
qcList <- Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint Constraint
c

  -- Now try continuing with each set and pick the first one that has
  -- a solution.
  [Sem r S] -> Sem r S
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
[Sem r a] -> Sem r a
asum' (((TyVarInfoMap, [SimpleConstraint]) -> Sem r S)
-> [(TyVarInfoMap, [SimpleConstraint])] -> [Sem r S]
forall a b. (a -> b) -> [a] -> [b]
map ((TyVarInfoMap -> [SimpleConstraint] -> Sem r S)
-> (TyVarInfoMap, [SimpleConstraint]) -> Sem r S
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TyVarInfoMap -> [SimpleConstraint] -> Sem r S
forall (r :: [(* -> *) -> * -> *]).
Members
  '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r =>
TyVarInfoMap -> [SimpleConstraint] -> Sem r S
solveConstraintChoice) [(TyVarInfoMap, [SimpleConstraint])]
qcList)

solveConstraintChoice
  :: Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r
  => TyVarInfoMap -> [SimpleConstraint] -> Sem r S
solveConstraintChoice :: TyVarInfoMap -> [SimpleConstraint] -> Sem r S
solveConstraintChoice TyVarInfoMap
quals [SimpleConstraint]
cs = do

  TyVarInfoMap -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
quals
  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat ((SimpleConstraint -> Sem r Doc)
-> [SimpleConstraint] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map SimpleConstraint -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]). Pretty t => t -> Sem r Doc
pretty' [SimpleConstraint]
cs)

  TyDefCtx
tyDefns <- forall (r :: [(* -> *) -> * -> *]).
Member (Input TyDefCtx) r =>
Sem r TyDefCtx
forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx

  -- Step 2. Check for weak unification to ensure termination. (a la
  -- Traytel et al).

  let toEqn :: SimpleConstraint -> (Type, Type)
toEqn (Type
t1 :<: Type
t2) = (Type
t1,Type
t2)
      toEqn (Type
t1 :=: Type
t2) = (Type
t1,Type
t2)
  S
_ <- SolveError -> Maybe S -> Sem r S
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Maybe a -> Sem r a
note SolveError
NoWeakUnifier (Maybe S -> Sem r S) -> Maybe S -> Sem r S
forall a b. (a -> b) -> a -> b
$ TyDefCtx -> [(Type, Type)] -> Maybe S
weakUnify TyDefCtx
tyDefns ((SimpleConstraint -> (Type, Type))
-> [SimpleConstraint] -> [(Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map SimpleConstraint -> (Type, Type)
toEqn [SimpleConstraint]
cs)

  -- Step 3. Simplify constraints, resulting in a set of atomic
  -- subtyping constraints.  Also simplify/update qualifier set
  -- accordingly.

  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"------------------------------"
  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Running simplifier..."

  (TyVarInfoMap
vm, [(Atom, Atom)]
atoms, S
theta_simp) <- TyVarInfoMap
-> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError, Output Message, Input TyDefCtx] r =>
TyVarInfoMap
-> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
simplify TyVarInfoMap
quals [SimpleConstraint]
cs
  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Done running simplifier. Results:"

  TyVarInfoMap -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
vm
  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat ([Sem r Doc] -> Sem r Doc) -> [Sem r Doc] -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ ((Atom, Atom) -> Sem r Doc) -> [(Atom, Atom)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (SimpleConstraint -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]). Pretty t => t -> Sem r Doc
pretty' (SimpleConstraint -> Sem r Doc)
-> ((Atom, Atom) -> SimpleConstraint) -> (Atom, Atom) -> Sem r Doc
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
  S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_simp

  -- Step 4. Turn the atomic constraints into a directed constraint
  -- graph.

  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"------------------------------"
  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Generating constraint graph..."

  -- Some variables might have qualifiers but not participate in any
  -- equality or subtyping relations (see issue #153); make sure to
  -- extract them and include them in the constraint graph as isolated
  -- vertices
  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 = [Atom] -> Set Atom
forall a. Ord a => [a] -> Set a
S.fromList ([Atom] -> Set Atom)
-> (TyVarInfoMap -> [Atom]) -> TyVarInfoMap -> Set Atom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name Type, TyVarInfo) -> Atom)
-> [(Name Type, TyVarInfo)] -> [Atom]
forall a b. (a -> b) -> [a] -> [b]
map ((Name Type, First Ilk) -> Atom
mkAVar ((Name Type, First Ilk) -> Atom)
-> ((Name Type, TyVarInfo) -> (Name Type, First Ilk))
-> (Name Type, TyVarInfo)
-> Atom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVarInfo -> First Ilk)
-> (Name Type, TyVarInfo) -> (Name Type, First Ilk)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Getting (First Ilk) TyVarInfo (First Ilk) -> TyVarInfo -> First Ilk
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (First Ilk) TyVarInfo (First Ilk)
Lens' TyVarInfo (First Ilk)
tyVarIlk)) ([(Name Type, TyVarInfo)] -> [Atom])
-> (TyVarInfoMap -> [(Name Type, TyVarInfo)])
-> TyVarInfoMap
-> [Atom]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Name Type) TyVarInfo -> [(Name Type, TyVarInfo)]
forall k a. Map k a -> [(k, a)]
M.assocs (Map (Name Type) TyVarInfo -> [(Name Type, TyVarInfo)])
-> (TyVarInfoMap -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap
-> [(Name Type, TyVarInfo)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM (TyVarInfoMap -> Set Atom) -> TyVarInfoMap -> Set Atom
forall a b. (a -> b) -> a -> b
$ TyVarInfoMap
vm
      g :: Graph Atom
g = Set Atom -> [(Atom, Atom)] -> Graph Atom
forall a. (Show a, Ord a) => Set a -> [(a, a)] -> Graph a
mkConstraintGraph Set Atom
vars [(Atom, Atom)]
atoms

  Graph Atom -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty Graph Atom
g

  -- Step 5.
  -- Check for any weakly connected components containing more
  -- than one skolem, or a skolem and a base type; such components are
  -- not allowed.  Other WCCs with a single skolem simply unify to
  -- that skolem.

  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"------------------------------"
  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Checking WCCs for skolems..."

  (Graph UAtom
g', S
theta_skolem) <- TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError, Output Message, Input TyDefCtx] r =>
TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
checkSkolems TyVarInfoMap
vm Graph Atom
g
  S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_skolem

  -- We don't need to ensure that theta_skolem respects sorts since
  -- checkSkolems will only unify skolem vars with unsorted variables.


  -- Step 6. Eliminate cycles from the graph, turning each strongly
  -- connected component into a single node, unifying all the atoms in
  -- each component.

  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"------------------------------"
  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Collapsing SCCs..."

  (Graph UAtom
g'', S
theta_cyc) <- TyDefCtx -> Graph UAtom -> Sem r (Graph UAtom, S)
forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError] r =>
TyDefCtx -> Graph UAtom -> Sem r (Graph UAtom, S)
elimCycles TyDefCtx
tyDefns Graph UAtom
g'

  Graph UAtom -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty Graph UAtom
g''
  S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_cyc

  -- Check that the resulting substitution respects sorts...
  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                        = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"Impossible! sortOK " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Name Type, Type) -> String
forall a. Show a => a -> String
show (Name Type, Type)
p
  Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (((Name Type, Type) -> Bool) -> [(Name Type, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Name Type, Type) -> Bool
sortOK (S -> [(Name Type, Type)]
forall a. Substitution a -> [(Name a, a)]
Subst.toList S
theta_cyc))
    (Sem r () -> Sem r ()) -> Sem r () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ SolveError -> Sem r ()
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify

  -- ... and update the sort map if we unified any type variables.
  -- Just make sure that if theta_cyc maps x |-> y, then y picks up
  -- the sort of x.

  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Old sort map:"
  TyVarInfoMap -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
vm

  let vm' :: TyVarInfoMap
vm' = ((Name Type, Type) -> TyVarInfoMap -> TyVarInfoMap)
-> TyVarInfoMap -> [(Name Type, Type)] -> TyVarInfoMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name Type, Type) -> TyVarInfoMap -> TyVarInfoMap
updateVarMap TyVarInfoMap
vm (S -> [(Name Type, Type)]
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

  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Updated sort map:"
  TyVarInfoMap -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
vm

  -- Steps 7 & 8: solve the graph, iteratively finding satisfying
  -- assignments for each type variable based on its successor and
  -- predecessor base types in the graph; then unify all the type
  -- variables in any remaining weakly connected components.

  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"------------------------------"
  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Solving for type variables..."

  S
theta_sol       <- TyVarInfoMap -> Graph UAtom -> Sem r S
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output Message] r =>
TyVarInfoMap -> Graph UAtom -> Sem r S
solveGraph TyVarInfoMap
vm' Graph UAtom
g''
  S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_sol

  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"------------------------------"
  Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug Sem r Doc
"Composing final substitution..."

  let theta_final :: S
theta_final = S
theta_sol S -> S -> S
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ S
theta_cyc S -> S -> S
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ S
theta_skolem S -> S -> S
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ S
theta_simp
  S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_final

  S -> Sem r S
forall (m :: * -> *) a. Monad m => a -> m a
return S
theta_final


--------------------------------------------------
-- Step 1. Constraint decomposition.

decomposeConstraint
  :: Members '[Fresh, Error SolveError, Input TyDefCtx] r
  => Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint :: Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint (CSub Type
t1 Type
t2) = [(TyVarInfoMap, [SimpleConstraint])]
-> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (m :: * -> *) a. Monad m => a -> m a
return [(TyVarInfoMap
forall a. Monoid a => a
mempty, [Type
t1 Type -> Type -> SimpleConstraint
:<: Type
t2])]
decomposeConstraint (CEq  Type
t1 Type
t2) = [(TyVarInfoMap, [SimpleConstraint])]
-> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (m :: * -> *) a. Monad m => a -> m a
return [(TyVarInfoMap
forall a. Monoid a => a
mempty, [Type
t1 Type -> Type -> SimpleConstraint
:=: Type
t2])]
decomposeConstraint (CQual Qualifier
q Type
ty) = ((TyVarInfoMap, [SimpleConstraint])
-> [(TyVarInfoMap, [SimpleConstraint])]
-> [(TyVarInfoMap, [SimpleConstraint])]
forall a. a -> [a] -> [a]
:[]) ((TyVarInfoMap, [SimpleConstraint])
 -> [(TyVarInfoMap, [SimpleConstraint])])
-> (TyVarInfoMap -> (TyVarInfoMap, [SimpleConstraint]))
-> TyVarInfoMap
-> [(TyVarInfoMap, [SimpleConstraint])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, []) (TyVarInfoMap -> [(TyVarInfoMap, [SimpleConstraint])])
-> Sem r TyVarInfoMap -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Qualifier -> Sem r TyVarInfoMap
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Type -> Qualifier -> Sem r TyVarInfoMap
decomposeQual Type
ty Qualifier
q
decomposeConstraint (CAnd [Constraint]
cs)    = ([(TyVarInfoMap, [SimpleConstraint])]
 -> (TyVarInfoMap, [SimpleConstraint]))
-> [[(TyVarInfoMap, [SimpleConstraint])]]
-> [(TyVarInfoMap, [SimpleConstraint])]
forall a b. (a -> b) -> [a] -> [b]
map [(TyVarInfoMap, [SimpleConstraint])]
-> (TyVarInfoMap, [SimpleConstraint])
forall a. Monoid a => [a] -> a
mconcat ([[(TyVarInfoMap, [SimpleConstraint])]]
 -> [(TyVarInfoMap, [SimpleConstraint])])
-> ([[(TyVarInfoMap, [SimpleConstraint])]]
    -> [[(TyVarInfoMap, [SimpleConstraint])]])
-> [[(TyVarInfoMap, [SimpleConstraint])]]
-> [(TyVarInfoMap, [SimpleConstraint])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(TyVarInfoMap, [SimpleConstraint])]]
-> [[(TyVarInfoMap, [SimpleConstraint])]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([[(TyVarInfoMap, [SimpleConstraint])]]
 -> [(TyVarInfoMap, [SimpleConstraint])])
-> Sem r [[(TyVarInfoMap, [SimpleConstraint])]]
-> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])])
-> [Constraint] -> Sem r [[(TyVarInfoMap, [SimpleConstraint])]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
decomposeConstraint [Constraint]
cs
decomposeConstraint Constraint
CTrue        = [(TyVarInfoMap, [SimpleConstraint])]
-> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (m :: * -> *) a. Monad m => a -> m a
return [(TyVarInfoMap, [SimpleConstraint])
forall a. Monoid a => a
mempty]
decomposeConstraint (CAll Bind [Name Type] Constraint
ty)    = do
  ([Name Type]
vars, Constraint
c) <- Bind [Name Type] Constraint -> Sem r ([Name Type], Constraint)
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' = [(Name Type, Type)] -> Constraint -> Constraint
forall b a. Subst b a => [(Name b, b)] -> a -> a
substs ([Name Type] -> [(Name Type, Type)]
mkSkolems [Name Type]
vars) Constraint
c
  (((TyVarInfoMap, [SimpleConstraint])
 -> (TyVarInfoMap, [SimpleConstraint]))
-> [(TyVarInfoMap, [SimpleConstraint])]
-> [(TyVarInfoMap, [SimpleConstraint])]
forall a b. (a -> b) -> [a] -> [b]
map (((TyVarInfoMap, [SimpleConstraint])
  -> (TyVarInfoMap, [SimpleConstraint]))
 -> [(TyVarInfoMap, [SimpleConstraint])]
 -> [(TyVarInfoMap, [SimpleConstraint])])
-> ([Name Type]
    -> (TyVarInfoMap, [SimpleConstraint])
    -> (TyVarInfoMap, [SimpleConstraint]))
-> [Name Type]
-> [(TyVarInfoMap, [SimpleConstraint])]
-> [(TyVarInfoMap, [SimpleConstraint])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVarInfoMap -> TyVarInfoMap)
-> (TyVarInfoMap, [SimpleConstraint])
-> (TyVarInfoMap, [SimpleConstraint])
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((TyVarInfoMap -> TyVarInfoMap)
 -> (TyVarInfoMap, [SimpleConstraint])
 -> (TyVarInfoMap, [SimpleConstraint]))
-> ([Name Type] -> TyVarInfoMap -> TyVarInfoMap)
-> [Name Type]
-> (TyVarInfoMap, [SimpleConstraint])
-> (TyVarInfoMap, [SimpleConstraint])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name Type] -> TyVarInfoMap -> TyVarInfoMap
addSkolems) [Name Type]
vars ([(TyVarInfoMap, [SimpleConstraint])]
 -> [(TyVarInfoMap, [SimpleConstraint])])
-> Sem r [(TyVarInfoMap, [SimpleConstraint])]
-> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
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 = (Name Type -> (Name Type, Type))
-> [Name Type] -> [(Name Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Name Type
forall a. a -> a
id (Name Type -> Name Type)
-> (Name Type -> Type) -> Name Type -> (Name Type, Type)
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)     = [[(TyVarInfoMap, [SimpleConstraint])]]
-> [(TyVarInfoMap, [SimpleConstraint])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(TyVarInfoMap, [SimpleConstraint])]]
 -> [(TyVarInfoMap, [SimpleConstraint])])
-> Sem r [[(TyVarInfoMap, [SimpleConstraint])]]
-> Sem r [(TyVarInfoMap, [SimpleConstraint])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sem r [(TyVarInfoMap, [SimpleConstraint])]]
-> Sem r [[(TyVarInfoMap, [SimpleConstraint])]]
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
[Sem r a] -> Sem r [a]
filterErrors ((Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])])
-> [Constraint] -> [Sem r [(TyVarInfoMap, [SimpleConstraint])]]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])]
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 :: Type -> Qualifier -> Sem r TyVarInfoMap
decomposeQual = Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go Set (String, [Type], Qualifier)
forall a. Set a
S.empty
  where
    go :: Members '[Fresh, Error SolveError, Input TyDefCtx] r
       => Set (String, [Type], Qualifier) -> Type -> Qualifier -> Sem r TyVarInfoMap

    -- For a type atom, call out to checkQual.
    go :: Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go Set (String, [Type], Qualifier)
_ (TyAtom Atom
a) Qualifier
q = Qualifier -> Atom -> Sem r TyVarInfoMap
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError] r =>
Qualifier -> Atom -> Sem r TyVarInfoMap
checkQual Qualifier
q Atom
a

    -- Coinductively check user-defined types for a qualifier.  Keep
    -- track of a set of user-defined types and qualifiers we have
    -- seen.  Every time we encounter a new one, add it to the set and
    -- recurse on its unfolding.  If we ever encounter one we have
    -- already seen, we can assume by coinduction that the qualifier
    -- is satisfied.
    go Set (String, [Type], Qualifier)
seen (TyCon (CUser String
t) [Type]
tys) Qualifier
q = do
      case (String
t, [Type]
tys, Qualifier
q) (String, [Type], Qualifier)
-> Set (String, [Type], Qualifier) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set (String, [Type], Qualifier)
seen of
        Bool
True -> TyVarInfoMap -> Sem r TyVarInfoMap
forall (m :: * -> *) a. Monad m => a -> m a
return TyVarInfoMap
forall a. Monoid a => a
mempty
        Bool
False -> do
          TyDefCtx
tyDefns <- forall (r :: [(* -> *) -> * -> *]).
Member (Input TyDefCtx) r =>
Sem r TyDefCtx
forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
          case String -> TyDefCtx -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
t TyDefCtx
tyDefns of
            Maybe TyDefBody
Nothing  -> String -> Sem r TyVarInfoMap
forall a. HasCallStack => String -> a
error (String -> Sem r TyVarInfoMap) -> String -> Sem r TyVarInfoMap
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. Show a => a -> String
show String
t String -> ShowS
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
              Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go ((String, [Type], Qualifier)
-> Set (String, [Type], Qualifier)
-> Set (String, [Type], Qualifier)
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

    -- If we have a container type where the container is still a variable,
    -- just replace it with List for the purposes of generating constraints---
    -- all containers (lists, bags, sets) have the same qualifier rules.
    go Set (String, [Type], Qualifier)
seen (TyCon (CContainer (AVar Var
_)) [Type]
tys) Qualifier
q = Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
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

    -- Otherwise, decompose a type constructor according to the qualRules.
    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 -> SolveError -> Sem r TyVarInfoMap
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw (SolveError -> Sem r TyVarInfoMap)
-> SolveError -> Sem r TyVarInfoMap
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> SolveError
Unqual Qualifier
q Type
ty
      Just [Maybe Qualifier]
qs -> [TyVarInfoMap] -> TyVarInfoMap
forall a. Monoid a => [a] -> a
mconcat ([TyVarInfoMap] -> TyVarInfoMap)
-> Sem r [TyVarInfoMap] -> Sem r TyVarInfoMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> Maybe Qualifier -> Sem r TyVarInfoMap)
-> [Type] -> [Maybe Qualifier] -> Sem r [TyVarInfoMap]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Sem r TyVarInfoMap
-> (Qualifier -> Sem r TyVarInfoMap)
-> Maybe Qualifier
-> Sem r TyVarInfoMap
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TyVarInfoMap -> Sem r TyVarInfoMap
forall (m :: * -> *) a. Monad m => a -> m a
return TyVarInfoMap
forall a. Monoid a => a
mempty) ((Qualifier -> Sem r TyVarInfoMap)
 -> Maybe Qualifier -> Sem r TyVarInfoMap)
-> (Type -> Qualifier -> Sem r TyVarInfoMap)
-> Type
-> Maybe Qualifier
-> Sem r TyVarInfoMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
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 :: Qualifier -> Atom -> Sem r TyVarInfoMap
checkQual Qualifier
q (AVar (U Name Type
v)) = TyVarInfoMap -> Sem r TyVarInfoMap
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVarInfoMap -> Sem r TyVarInfoMap)
-> (TyVarInfo -> TyVarInfoMap) -> TyVarInfo -> Sem r TyVarInfoMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Name Type) TyVarInfo -> TyVarInfoMap
VM (Map (Name Type) TyVarInfo -> TyVarInfoMap)
-> (TyVarInfo -> Map (Name Type) TyVarInfo)
-> TyVarInfo
-> TyVarInfoMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name Type -> TyVarInfo -> Map (Name Type) TyVarInfo
forall k a. k -> a -> Map k a
M.singleton Name Type
v (TyVarInfo -> Sem r TyVarInfoMap)
-> TyVarInfo -> Sem r TyVarInfoMap
forall a b. (a -> b) -> a -> b
$ Ilk -> Sort -> TyVarInfo
mkTVI Ilk
Unification (Qualifier -> Sort
forall a. a -> Set a
S.singleton Qualifier
q)
checkQual Qualifier
q (AVar (S Name Type
v)) = SolveError -> Sem r TyVarInfoMap
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw (SolveError -> Sem r TyVarInfoMap)
-> SolveError -> Sem r TyVarInfoMap
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  -> TyVarInfoMap -> Sem r TyVarInfoMap
forall (m :: * -> *) a. Monad m => a -> m a
return TyVarInfoMap
forall a. Monoid a => a
mempty
    Bool
False -> SolveError -> Sem r TyVarInfoMap
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw (SolveError -> Sem r TyVarInfoMap)
-> SolveError -> Sem r TyVarInfoMap
forall a b. (a -> b) -> a -> b
$ Qualifier -> BaseTy -> SolveError
UnqualBase Qualifier
q BaseTy
bty

--------------------------------------------------
-- Step 3. Constraint simplification.

-- | This step does unification of equality constraints, as well as
--   structural decomposition of subtyping constraints.  For example,
--   if we have a constraint (x -> y) <: (z -> Int), then we can
--   decompose it into two constraints, (z <: x) and (y <: Int); if we
--   have a constraint v <: (a,b), then we substitute v ↦ (x,y) (where
--   x and y are fresh type variables) and continue; and so on.
--
--   After this step, the remaining constraints will all be atomic
--   constraints, that is, only of the form (v1 <: v2), (v <: b), or
--   (b <: v), where v is a type variable and b is a base type.

simplify
  :: Members '[Error SolveError, Output Message, Input TyDefCtx] r
  => TyVarInfoMap -> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
simplify :: TyVarInfoMap
-> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
simplify TyVarInfoMap
origVM [SimpleConstraint]
cs
  = (\(SS TyVarInfoMap
vm' [SimpleConstraint]
cs' S
s' Set SimpleConstraint
_) -> (TyVarInfoMap
vm', (SimpleConstraint -> (Atom, Atom))
-> [SimpleConstraint] -> [(Atom, Atom)]
forall a b. (a -> b) -> [a] -> [b]
map SimpleConstraint -> (Atom, Atom)
extractAtoms [SimpleConstraint]
cs', S
s'))
  -- contFreshMT :: Monad m => FreshMT m a -> Integer -> m a
  -- "Run a FreshMT computation given a starting index for fresh name generation."
  (SimplifyState -> (TyVarInfoMap, [(Atom, Atom)], S))
-> Sem r SimplifyState -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Sem (Fresh : r) SimplifyState -> Sem r SimplifyState
forall (r :: [(* -> *) -> * -> *]) a.
Integer -> Sem (Fresh : r) a -> Sem r a
runFresh' Integer
n (SimplifyState
-> Sem (State SimplifyState : Fresh : r) ()
-> Sem (Fresh : r) SimplifyState
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 S
forall a. Substitution a
idS Set SimpleConstraint
forall a. Set a
S.empty) Sem (State SimplifyState : Fresh : r) ()
forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Output Message,
    Input TyDefCtx]
  r =>
Sem r ()
simplify')
  where

    fvNums :: Alpha a => [a] -> [Integer]
    fvNums :: [a] -> [Integer]
fvNums = (Name Type -> Integer) -> [Name Type] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Integer
forall a. Name a -> Integer
name2Integer :: Name Type -> Integer) ([Name Type] -> [Integer])
-> ([a] -> [Name Type]) -> [a] -> [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (Endo [Name Type]) [a] (Name Type) -> [a] -> [Name Type]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [Name Type]) [a] (Name Type)
forall a (f :: * -> *) b.
(Alpha a, Typeable b, Contravariant f, Applicative f) =>
(Name b -> f (Name b)) -> a -> f a
fv

    -- Find first unused integer in constraint free vars and sort map
    -- domain, and use it to start the fresh var generation, so we don't
    -- generate any "fresh" names that interfere with existing names
    n1 :: Integer
n1 = [Integer] -> Integer
forall p. (Num p, Ord p) => [p] -> p
maximum0 ([Integer] -> Integer)
-> ([SimpleConstraint] -> [Integer])
-> [SimpleConstraint]
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SimpleConstraint] -> [Integer]
forall a. Alpha a => [a] -> [Integer]
fvNums ([SimpleConstraint] -> Integer) -> [SimpleConstraint] -> Integer
forall a b. (a -> b) -> a -> b
$ [SimpleConstraint]
cs
    n :: Integer
n = Integer -> Integer
forall a. Enum a => a -> a
succ (Integer -> Integer)
-> (TyVarInfoMap -> Integer) -> TyVarInfoMap -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Integer] -> Integer)
-> (TyVarInfoMap -> [Integer]) -> TyVarInfoMap -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer
n1Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
:) ([Integer] -> [Integer])
-> (TyVarInfoMap -> [Integer]) -> TyVarInfoMap -> [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name Type] -> [Integer]
forall a. Alpha a => [a] -> [Integer]
fvNums ([Name Type] -> [Integer])
-> (TyVarInfoMap -> [Name Type]) -> TyVarInfoMap -> [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Name Type) TyVarInfo -> [Name Type]
forall k a. Map k a -> [k]
M.keys (Map (Name Type) TyVarInfo -> [Name Type])
-> (TyVarInfoMap -> Map (Name Type) TyVarInfo)
-> TyVarInfoMap
-> [Name Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM (TyVarInfoMap -> Integer) -> TyVarInfoMap -> Integer
forall a b. (a -> b) -> a -> b
$ TyVarInfoMap
origVM

    maximum0 :: [p] -> p
maximum0 [] = p
0
    maximum0 [p]
xs = [p] -> p
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [p]
xs

    -- Extract the type atoms from an atomic constraint.
    extractAtoms :: SimpleConstraint -> (Atom, Atom)
    extractAtoms :: SimpleConstraint -> (Atom, Atom)
extractAtoms (TyAtom Atom
a1 :<: TyAtom Atom
a2) = (Atom
a1, Atom
a2)
    extractAtoms SimpleConstraint
c = String -> (Atom, Atom)
forall a. HasCallStack => String -> a
error (String -> (Atom, Atom)) -> String -> (Atom, Atom)
forall a b. (a -> b) -> a -> b
$ String
"Impossible: simplify left non-atomic or non-subtype constraint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SimpleConstraint -> String
forall a. Show a => a -> String
show SimpleConstraint
c

    -- Iterate picking one simplifiable constraint and simplifying it
    -- until none are left.
    simplify'
      :: Members '[State SimplifyState, Fresh, Error SolveError, Output Message, Input TyDefCtx] r
      => Sem r ()
    simplify' :: Sem r ()
simplify' = do
      -- q <- gets fst
      -- debug (pretty q)
      -- debug ""

      Maybe SimpleConstraint
mc <- Sem r (Maybe SimpleConstraint)
forall (r :: [(* -> *) -> * -> *]).
Members '[State SimplifyState, Fresh, Error SolveError] r =>
Sem r (Maybe SimpleConstraint)
pickSimplifiable
      case Maybe SimpleConstraint
mc of
        Maybe SimpleConstraint
Nothing -> () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Just SimpleConstraint
s  -> do

          Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"Simplifying:" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> SimpleConstraint -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]). Pretty t => t -> Sem r Doc
pretty' SimpleConstraint
s

          SimpleConstraint -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
  r =>
SimpleConstraint -> Sem r ()
simplifyOne SimpleConstraint
s
          Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Output Message,
    Input TyDefCtx]
  r =>
Sem r ()
simplify'

    -- Pick out one simplifiable constraint, removing it from the list
    -- of constraints in the state.  Return Nothing if no more
    -- constraints can be simplified.
    pickSimplifiable
      :: Members '[State SimplifyState, Fresh, Error SolveError] r
      => Sem r (Maybe SimpleConstraint)
    pickSimplifiable :: Sem r (Maybe SimpleConstraint)
pickSimplifiable = do
      [SimpleConstraint]
curCs <- Getter SimplifyState [SimpleConstraint] -> Sem r [SimpleConstraint]
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' SimplifyState [SimpleConstraint]
Getter SimplifyState [SimpleConstraint]
ssConstraints
      case (SimpleConstraint -> Bool)
-> [SimpleConstraint]
-> Maybe (SimpleConstraint, [SimpleConstraint])
forall a. (a -> Bool) -> [a] -> Maybe (a, [a])
pick SimpleConstraint -> Bool
simplifiable [SimpleConstraint]
curCs of
        Maybe (SimpleConstraint, [SimpleConstraint])
Nothing     -> Maybe SimpleConstraint -> Sem r (Maybe SimpleConstraint)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SimpleConstraint
forall a. Maybe a
Nothing
        Just (SimpleConstraint
a,[SimpleConstraint]
as) -> do
          Lens' SimplifyState [SimpleConstraint]
ssConstraints Lens' SimplifyState [SimpleConstraint]
-> [SimpleConstraint] -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> a -> Sem r ()
.= [SimpleConstraint]
as
          Maybe SimpleConstraint -> Sem r (Maybe SimpleConstraint)
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleConstraint -> Maybe SimpleConstraint
forall a. a -> Maybe a
Just SimpleConstraint
a)

    -- Pick the first element from a list satisfying the given
    -- predicate, returning the element and the list with the element
    -- removed.
    pick :: (a -> Bool) -> [a] -> Maybe (a,[a])
    pick :: (a -> Bool) -> [a] -> Maybe (a, [a])
pick a -> Bool
_ [] = Maybe (a, [a])
forall a. Maybe a
Nothing
    pick a -> Bool
p (a
a:[a]
as)
      | a -> Bool
p a
a       = (a, [a]) -> Maybe (a, [a])
forall a. a -> Maybe a
Just (a
a,[a]
as)
      | Bool
otherwise = ([a] -> [a]) -> (a, [a]) -> (a, [a])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ((a, [a]) -> (a, [a])) -> Maybe (a, [a]) -> Maybe (a, [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> Bool) -> [a] -> Maybe (a, [a])
forall a. (a -> Bool) -> [a] -> Maybe (a, [a])
pick a -> Bool
p [a]
as

    -- Check if a constraint can be simplified.  An equality
    -- constraint can always be "simplified" via unification.  A
    -- subtyping constraint can be simplified if either it involves a
    -- type constructor (in which case we can decompose it), or if it
    -- involves two base types (in which case it can be removed if the
    -- relationship holds).
    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

    -- Simplify the given simplifiable constraint.  If the constraint
    -- has already been seen before (due to expansion of a recursive
    -- type), just throw it away and stop.
    simplifyOne
      :: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r
      => SimpleConstraint -> Sem r ()
    simplifyOne :: SimpleConstraint -> Sem r ()
simplifyOne SimpleConstraint
c = do
      Set SimpleConstraint
seen <- Getter SimplifyState (Set SimpleConstraint)
-> Sem r (Set SimpleConstraint)
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' SimplifyState (Set SimpleConstraint)
Getter SimplifyState (Set SimpleConstraint)
ssSeen
      case SimpleConstraint
c SimpleConstraint -> Set SimpleConstraint -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set SimpleConstraint
seen of
        Bool
True  -> () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Bool
False -> do
          Lens' SimplifyState (Set SimpleConstraint)
ssSeen Lens' SimplifyState (Set SimpleConstraint)
-> (Set SimpleConstraint -> Set SimpleConstraint) -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= SimpleConstraint -> Set SimpleConstraint -> Set SimpleConstraint
forall a. Ord a => a -> Set a -> Set a
S.insert SimpleConstraint
c
          SimpleConstraint -> Sem r ()
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 ()

    -- If we have an equality constraint, run unification on it.  The
    -- resulting substitution is applied to the remaining constraints
    -- as well as prepended to the current substitution.

    simplifyOne' :: SimpleConstraint -> Sem r ()
simplifyOne' (Type
ty1 :=: Type
ty2) = do
      TyDefCtx
tyDefns <- forall (r :: [(* -> *) -> * -> *]).
Member (Input TyDefCtx) r =>
Sem r TyDefCtx
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 -> SolveError -> Sem r ()
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
        Just S
s' -> S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
  r =>
S -> Sem r ()
extendSubst S
s'

    -- If we see a constraint of the form (T <: a), where T is a
    -- user-defined type and a is a type variable, then just turn it
    -- into an equality (T = a).  This is sound but probably not
    -- complete.  The alternative seems quite complicated, possibly
    -- even undecidable.  See https://github.com/disco-lang/disco/issues/207 .
    simplifyOne' (ty1 :: Type
ty1@(TyCon (CUser String
_) [Type]
_) :<: ty2 :: Type
ty2@TyVar{})
      = SimpleConstraint -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
  r =>
SimpleConstraint -> Sem r ()
simplifyOne' (Type
ty1 Type -> Type -> SimpleConstraint
:=: Type
ty2)

    -- Otherwise, expand the user-defined type and continue.
    simplifyOne' (TyCon (CUser String
t) [Type]
ts :<: Type
ty2) = do
      TyDefCtx
tyDefns <- forall (r :: [(* -> *) -> * -> *]).
Member (Input TyDefCtx) r =>
Sem r TyDefCtx
forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
      case String -> TyDefCtx -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
t TyDefCtx
tyDefns of
        Maybe TyDefBody
Nothing  -> String -> Sem r ()
forall a. HasCallStack => String -> a
error (String -> Sem r ()) -> String -> Sem r ()
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. Show a => a -> String
show String
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not in ty defn map!"
        Just (TyDefBody [String]
_ [Type] -> Type
body) ->
          Lens' SimplifyState [SimpleConstraint]
ssConstraints Lens' SimplifyState [SimpleConstraint]
-> ([SimpleConstraint] -> [SimpleConstraint]) -> Sem r ()
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) SimpleConstraint -> [SimpleConstraint] -> [SimpleConstraint]
forall a. a -> [a] -> [a]
:)

    -- Turn  a <: T  into  a = T.  See comment above.
    simplifyOne' (ty1 :: Type
ty1@TyVar{} :<: ty2 :: Type
ty2@(TyCon (CUser String
_) [Type]
_))
      = SimpleConstraint -> Sem r ()
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 (r :: [(* -> *) -> * -> *]).
Member (Input TyDefCtx) r =>
Sem r TyDefCtx
forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
      case String -> TyDefCtx -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
t TyDefCtx
tyDefns of
        Maybe TyDefBody
Nothing  -> String -> Sem r ()
forall a. HasCallStack => String -> a
error (String -> Sem r ()) -> String -> Sem r ()
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. Show a => a -> String
show String
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not in ty defn map!"
        Just (TyDefBody [String]
_ [Type] -> Type
body) ->
          Lens' SimplifyState [SimpleConstraint]
ssConstraints Lens' SimplifyState [SimpleConstraint]
-> ([SimpleConstraint] -> [SimpleConstraint]) -> Sem r ()
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) SimpleConstraint -> [SimpleConstraint] -> [SimpleConstraint]
forall a. a -> [a] -> [a]
:)

    -- Given a subtyping constraint between two type constructors,
    -- decompose it if the constructors are the same (or fail if they
    -- aren't), taking into account the variance of each argument to
    -- the constructor.  Container types are a special case;
    -- recursively generate a subtyping constraint for their
    -- constructors as well.
    simplifyOne' (TyCon c1 :: Con
c1@(CContainer Atom
ctr1) [Type]
tys1 :<: TyCon (CContainer Atom
ctr2) [Type]
tys2) =
      Lens' SimplifyState [SimpleConstraint]
ssConstraints Lens' SimplifyState [SimpleConstraint]
-> ([SimpleConstraint] -> [SimpleConstraint]) -> Sem r ()
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)
         SimpleConstraint -> [SimpleConstraint] -> [SimpleConstraint]
forall a. a -> [a] -> [a]
: (Variance -> Type -> Type -> SimpleConstraint)
-> [Variance] -> [Type] -> [Type] -> [SimpleConstraint]
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
         )
         [SimpleConstraint] -> [SimpleConstraint] -> [SimpleConstraint]
forall a. [a] -> [a] -> [a]
++)

    simplifyOne' (TyCon Con
c1 [Type]
tys1 :<: TyCon Con
c2 [Type]
tys2)
      | Con
c1 Con -> Con -> Bool
forall a. Eq a => a -> a -> Bool
/= Con
c2  = SolveError -> Sem r ()
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
      | Bool
otherwise =
          Lens' SimplifyState [SimpleConstraint]
ssConstraints Lens' SimplifyState [SimpleConstraint]
-> ([SimpleConstraint] -> [SimpleConstraint]) -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= ((Variance -> Type -> Type -> SimpleConstraint)
-> [Variance] -> [Type] -> [Type] -> [SimpleConstraint]
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 [SimpleConstraint] -> [SimpleConstraint] -> [SimpleConstraint]
forall a. [a] -> [a] -> [a]
++)

    -- Given a subtyping constraint between a variable and a type
    -- constructor, expand the variable into the same constructor
    -- applied to fresh type variables.
    simplifyOne' con :: SimpleConstraint
con@(TyVar Name Type
a   :<: TyCon Con
c [Type]
_) = Name Type -> Con -> SimpleConstraint -> Sem r ()
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  ) = Name Type -> Con -> SimpleConstraint -> Sem r ()
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

    -- Given a subtyping constraint between two base types, just check
    -- whether the first is indeed a subtype of the second.  (Note
    -- that we only pattern match here on type atoms, which could
    -- include variables, but this will only ever get called if
    -- 'simplifiable' was true, which checks that both are base
    -- types.)
    simplifyOne' (TyAtom (ABase BaseTy
b1) :<: TyAtom (ABase BaseTy
b2)) = do
      case BaseTy -> BaseTy -> Bool
isSubB BaseTy
b1 BaseTy
b2 of
        Bool
True  -> () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Bool
False -> SolveError -> Sem r ()
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify

    simplifyOne' (Type
s :<: Type
t) =
      String -> Sem r ()
forall a. HasCallStack => String -> a
error (String -> Sem r ()) -> String -> Sem r ()
forall a b. (a -> b) -> a -> b
$ String
"Impossible! simplifyOne' " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :<: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
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 :: Name Type -> Con -> SimpleConstraint -> Sem r ()
expandStruct Name Type
a Con
c SimpleConstraint
con = do
      [Type]
as <- (Variance -> Sem r Type) -> [Variance] -> Sem r [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sem r Type -> Variance -> Sem r Type
forall a b. a -> b -> a
const (Name Type -> Type
TyVar (Name Type -> Type) -> Sem r (Name Type) -> Sem r Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name Type -> Sem r (Name Type)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name Type
forall a. String -> Name a
string2Name String
"a"))) (Con -> [Variance]
arity Con
c)
      let s' :: S
s' = Name Type
a Name Type -> Type -> S
forall a. Name a -> a -> Substitution a
|-> Con -> [Type] -> Type
TyCon Con
c [Type]
as
      Lens' SimplifyState [SimpleConstraint]
ssConstraints Lens' SimplifyState [SimpleConstraint]
-> ([SimpleConstraint] -> [SimpleConstraint]) -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= (SimpleConstraint
conSimpleConstraint -> [SimpleConstraint] -> [SimpleConstraint]
forall a. a -> [a] -> [a]
:)
      S -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
  r =>
S -> Sem r ()
extendSubst S
s'

    -- 1. compose s' with current subst
    -- 2. apply s' to constraints
    -- 3. apply s' to qualifier map and decompose
    extendSubst
      :: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r
      => S -> Sem r ()
    extendSubst :: S -> Sem r ()
extendSubst S
s' = do
      Lens' SimplifyState S
ssSubst Lens' SimplifyState S -> (S -> S) -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= (S
s'S -> S -> S
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@)
      Lens' SimplifyState [SimpleConstraint]
ssConstraints Lens' SimplifyState [SimpleConstraint]
-> ([SimpleConstraint] -> [SimpleConstraint]) -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= S -> [SimpleConstraint] -> [SimpleConstraint]
forall b a. Subst b a => Substitution b -> a -> a
applySubst S
s'
      S -> Sem r ()
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 :: S -> Sem r ()
substVarMap S
s' = do
      TyVarInfoMap
vm <- Getter SimplifyState TyVarInfoMap -> Sem r TyVarInfoMap
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' SimplifyState TyVarInfoMap
Getter SimplifyState TyVarInfoMap
ssVarMap

      -- 1. Get quals for each var in domain of s' and match them with
      -- the types being substituted for those vars.

      let tySorts :: [(Type, Sort)]
          tySorts :: [(Type, Sort)]
tySorts = ((Type, TyVarInfo) -> (Type, Sort))
-> [(Type, TyVarInfo)] -> [(Type, Sort)]
forall a b. (a -> b) -> [a] -> [b]
map ((TyVarInfo -> Sort) -> (Type, TyVarInfo) -> (Type, Sort)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Getting Sort TyVarInfo Sort -> TyVarInfo -> Sort
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Sort TyVarInfo Sort
Lens' TyVarInfo Sort
tyVarSort)) ([(Type, TyVarInfo)] -> [(Type, Sort)])
-> ([(Name Type, Type)] -> [(Type, TyVarInfo)])
-> [(Name Type, Type)]
-> [(Type, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name Type, Type) -> Maybe (Type, TyVarInfo))
-> [(Name Type, Type)] -> [(Type, TyVarInfo)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Name Type -> Maybe TyVarInfo)
-> (Type, Name Type) -> Maybe (Type, TyVarInfo)
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) ((Type, Name Type) -> Maybe (Type, TyVarInfo))
-> ((Name Type, Type) -> (Type, Name Type))
-> (Name Type, Type)
-> Maybe (Type, TyVarInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name Type, Type) -> (Type, Name Type)
forall a b. (a, b) -> (b, a)
swap) ([(Name Type, Type)] -> [(Type, Sort)])
-> [(Name Type, Type)] -> [(Type, Sort)]
forall a b. (a -> b) -> a -> b
$ S -> [(Name Type, Type)]
forall a. Substitution a -> [(Name a, a)]
Subst.toList S
s'

          tyQualList :: [(Type, Qualifier)]
          tyQualList :: [(Type, Qualifier)]
tyQualList = ((Type, Sort) -> [(Type, Qualifier)])
-> [(Type, Sort)] -> [(Type, Qualifier)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Type, [Qualifier]) -> [(Type, Qualifier)]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA ((Type, [Qualifier]) -> [(Type, Qualifier)])
-> ((Type, Sort) -> (Type, [Qualifier]))
-> (Type, Sort)
-> [(Type, Qualifier)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort -> [Qualifier]) -> (Type, Sort) -> (Type, [Qualifier])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Sort -> [Qualifier]
forall a. Set a -> [a]
S.toList) [(Type, Sort)]
tySorts

      -- 2. Decompose the resulting qualifier constraints

      TyVarInfoMap
vm' <- [TyVarInfoMap] -> TyVarInfoMap
forall a. Monoid a => [a] -> a
mconcat ([TyVarInfoMap] -> TyVarInfoMap)
-> Sem r [TyVarInfoMap] -> Sem r TyVarInfoMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Type, Qualifier) -> Sem r TyVarInfoMap)
-> [(Type, Qualifier)] -> Sem r [TyVarInfoMap]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Type -> Qualifier -> Sem r TyVarInfoMap)
-> (Type, Qualifier) -> Sem r TyVarInfoMap
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Qualifier -> Sem r TyVarInfoMap
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Type -> Qualifier -> Sem r TyVarInfoMap
decomposeQual) [(Type, Qualifier)]
tyQualList

      -- 3. delete domain of s' from vm and merge in decomposed quals.

      Lens' SimplifyState TyVarInfoMap
ssVarMap Lens' SimplifyState TyVarInfoMap -> TyVarInfoMap -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> a -> Sem r ()
.= TyVarInfoMap
vm' TyVarInfoMap -> TyVarInfoMap -> TyVarInfoMap
forall a. Semigroup a => a -> a -> a
<> (TyVarInfoMap -> Name Type -> TyVarInfoMap)
-> TyVarInfoMap -> Set (Name Type) -> TyVarInfoMap
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Name Type -> TyVarInfoMap -> TyVarInfoMap)
-> TyVarInfoMap -> Name Type -> TyVarInfoMap
forall a b c. (a -> b -> c) -> b -> a -> c
flip Name Type -> TyVarInfoMap -> TyVarInfoMap
deleteVM) TyVarInfoMap
vm (S -> Set (Name Type)
forall a. Substitution a -> Set (Name a)
dom S
s')

      -- The above works even when unifying two variables.  Say we have
      -- the TyVarInfoMap
      --
      --   a |-> {add}
      --   b |-> {sub}
      --
      -- and we get back theta = [a |-> b].  The domain of theta
      -- consists solely of a, so we look up a in the TyVarInfoMap and get
      -- {add}.  We therefore generate the constraint 'add (theta a)'
      -- = 'add b' which can't be decomposed at all, and hence yields
      -- the TyVarInfoMap {b |-> {add}}.  We then delete a from the
      -- original TyVarInfoMap and merge the result with the new TyVarInfoMap,
      -- yielding {b |-> {sub,add}}.


    -- Create a subtyping constraint based on the variance of a type
    -- constructor argument position: in the usual order for
    -- covariant, and reversed for contravariant.
    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

--------------------------------------------------
-- Step 4: Build constraint graph

-- | Given a list of atoms and atomic subtype constraints (each pair
--   @(a1,a2)@ corresponds to the constraint @a1 <: a2@) build the
--   corresponding constraint graph.
mkConstraintGraph :: (Show a, Ord a) => Set a -> [(a, a)] -> Graph a
mkConstraintGraph :: Set a -> [(a, a)] -> Graph a
mkConstraintGraph Set a
as [(a, a)]
cs = Set a -> Set (a, a) -> Graph a
forall a. (Show a, Ord a) => Set a -> Set (a, a) -> Graph a
G.mkGraph Set a
nodes ([(a, a)] -> Set (a, a)
forall a. Ord a => [a] -> Set a
S.fromList [(a, a)]
cs)
  where
    nodes :: Set a
nodes = Set a
as Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`S.union` [a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList ([(a, a)]
cs [(a, a)] -> Getting (Endo [a]) [(a, a)] a -> [a]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. ((a, a) -> Const (Endo [a]) (a, a))
-> [(a, a)] -> Const (Endo [a]) [(a, a)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (((a, a) -> Const (Endo [a]) (a, a))
 -> [(a, a)] -> Const (Endo [a]) [(a, a)])
-> ((a -> Const (Endo [a]) a) -> (a, a) -> Const (Endo [a]) (a, a))
-> Getting (Endo [a]) [(a, a)] a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Const (Endo [a]) a) -> (a, a) -> Const (Endo [a]) (a, a)
forall s t a b. Each s t a b => Traversal s t a b
each)

--------------------------------------------------
-- Step 5: Check skolems

-- | Check for any weakly connected components containing more than
--   one skolem, or a skolem and a base type, or a skolem and any
--   variables with nontrivial sorts; such components are not allowed.
--   If there are any WCCs with a single skolem, no base types, and
--   only unsorted variables, just unify them all with the skolem and
--   remove those components.
checkSkolems
  :: Members '[Error SolveError, Output Message, Input TyDefCtx] r
  => TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
checkSkolems :: TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
checkSkolems TyVarInfoMap
vm Graph Atom
graph = do
  let skolemWCCs :: [Set Atom]
      skolemWCCs :: [Set Atom]
skolemWCCs = (Set Atom -> Bool) -> [Set Atom] -> [Set Atom]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Atom -> Bool) -> Set Atom -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Atom -> Bool
isSkolem) ([Set Atom] -> [Set Atom]) -> [Set Atom] -> [Set Atom]
forall a b. (a -> b) -> a -> b
$ Graph Atom -> [Set Atom]
forall a. Ord a => Graph a -> [Set a]
G.wcc Graph Atom
graph

      ok :: Set Atom -> Bool
ok Set Atom
wcc =  Set Atom -> Int
forall a. Set a -> Int
S.size ((Atom -> Bool) -> Set Atom -> Set Atom
forall a. (a -> Bool) -> Set a -> Set a
S.filter Atom -> Bool
isSkolem Set Atom
wcc) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1
             Bool -> Bool -> Bool
&& (Atom -> Bool) -> Set Atom -> 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) -> Bool -> (TyVarInfo -> Bool) -> Maybe TyVarInfo -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (Sort -> Bool
forall a. Set a -> Bool
S.null (Sort -> Bool) -> (TyVarInfo -> Sort) -> TyVarInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Sort TyVarInfo Sort -> TyVarInfo -> Sort
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Sort TyVarInfo Sort
Lens' TyVarInfo Sort
tyVarSort) (Name Type -> TyVarInfoMap -> Maybe TyVarInfo
lookupVM Name Type
v TyVarInfoMap
vm) })
                Set Atom
wcc

      ([Set Atom]
good, [Set Atom]
bad) = (Set Atom -> Bool) -> [Set Atom] -> ([Set Atom], [Set Atom])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Set Atom -> Bool
ok [Set Atom]
skolemWCCs

  Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Set Atom] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Set Atom]
bad) (Sem r () -> Sem r ()) -> Sem r () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ SolveError -> Sem r ()
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify

  -- take all good sets and
  --   (1) delete them from the graph
  --   (2) unify them all with the skolem
  Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError, Output Message, Input TyDefCtx] r =>
Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
graph S
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)) = String -> UAtom
forall a. HasCallStack => String -> a
error (String -> UAtom) -> String -> UAtom
forall a b. (a -> b) -> a -> b
$ String
"Skolem " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name Type -> String
forall a. Show a => a -> String
show Name Type
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" remaining in noSkolems"

    unifyWCCs
      :: Members '[Error SolveError, Output Message, Input TyDefCtx] r
      => Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
    unifyWCCs :: Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
g S
s []     = (Graph UAtom, S) -> Sem r (Graph UAtom, S)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Atom -> UAtom) -> Graph Atom -> Graph UAtom
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
      Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"Unifying" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> [Set Atom] -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]). Pretty t => t -> Sem r Doc
pretty' (Set Atom
uSet Atom -> [Set Atom] -> [Set Atom]
forall a. a -> [a] -> [a]
:[Set Atom]
us) Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc
"..."

      TyDefCtx
tyDefns <- forall (r :: [(* -> *) -> * -> *]).
Member (Input TyDefCtx) r =>
Sem r TyDefCtx
forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx

      let g' :: Graph Atom
g' = (Graph Atom -> Atom -> Graph Atom)
-> Graph Atom -> Set Atom -> Graph Atom
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Atom -> Graph Atom -> Graph Atom)
-> Graph Atom -> Atom -> Graph Atom
forall a b c. (a -> b -> c) -> b -> a -> c
flip Atom -> Graph Atom -> Graph Atom
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 (Set Atom -> [Atom]
forall a. Set a -> [a]
S.toList Set Atom
u)
      case Maybe (Substitution Atom)
ms' of
        Maybe (Substitution Atom)
Nothing -> SolveError -> Sem r (Graph UAtom, S)
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
        Just Substitution Atom
s' -> Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError, Output Message, Input TyDefCtx] r =>
Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
g' (Substitution Atom -> S
atomToTypeSubst Substitution Atom
s' S -> S -> S
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ S
s) [Set Atom]
us

--------------------------------------------------
-- Step 6: Eliminate cycles

-- | Eliminate cycles in the constraint set by collapsing each
--   strongly connected component to a single node, (unifying all the
--   types in the SCC). A strongly connected component is a maximal
--   set of nodes where every node is reachable from every other by a
--   directed path; since we are using directed edges to indicate a
--   subtyping constraint, this means every node must be a subtype of
--   every other, and the only way this can happen is if all are in
--   fact equal.
--
--   Of course, this step can fail if the types in a SCC are not
--   unifiable.  If it succeeds, it returns the collapsed graph (which
--   is now guaranteed to be acyclic, i.e. a DAG) and a substitution.
elimCycles
  :: Members '[Error SolveError] r
  => TyDefCtx -> Graph UAtom -> Sem r (Graph UAtom, S)
elimCycles :: TyDefCtx -> Graph UAtom -> Sem r (Graph UAtom, S)
elimCycles TyDefCtx
tyDefns = (Substitution UAtom -> S)
-> ([UAtom] -> Maybe (Substitution UAtom))
-> Graph UAtom
-> Sem r (Graph UAtom, S)
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 :: (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
  = SolveError
-> Maybe (Graph a, Substitution b)
-> Sem r (Graph a, Substitution b)
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Maybe a -> Sem r a
note SolveError
NoUnify
  (Maybe (Graph a, Substitution b)
 -> Sem r (Graph a, Substitution b))
-> Maybe (Graph a, Substitution b)
-> Sem r (Graph a, Substitution b)
forall a b. (a -> b) -> a -> b
$ (((a, Substitution a) -> a) -> Graph (a, Substitution a) -> Graph a
forall b a. Ord b => (a -> b) -> Graph a -> Graph b
G.map (a, Substitution a) -> a
forall a b. (a, b) -> a
fst (Graph (a, Substitution a) -> Graph a)
-> (Graph (a, Substitution a) -> Substitution b)
-> Graph (a, Substitution a)
-> (Graph a, Substitution b)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (Substitution a -> Substitution b
genSubst (Substitution a -> Substitution b)
-> (Graph (a, Substitution a) -> Substitution a)
-> Graph (a, Substitution a)
-> Substitution b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Substitution a) -> Substitution a
forall a (t :: * -> *).
(Subst a a, Foldable t) =>
t (Substitution a) -> Substitution a
compose (Set (Substitution a) -> Substitution a)
-> (Graph (a, Substitution a) -> Set (Substitution a))
-> Graph (a, Substitution a)
-> Substitution a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, Substitution a) -> Substitution a)
-> Set (a, Substitution a) -> Set (Substitution a)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (a, Substitution a) -> Substitution a
forall a b. (a, b) -> b
snd (Set (a, Substitution a) -> Set (Substitution a))
-> (Graph (a, Substitution a) -> Set (a, Substitution a))
-> Graph (a, Substitution a)
-> Set (Substitution a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph (a, Substitution a) -> Set (a, Substitution a)
forall a. Graph a -> Set a
G.nodes)) (Graph (a, Substitution a) -> (Graph a, Substitution b))
-> Maybe (Graph (a, Substitution a))
-> Maybe (Graph a, Substitution b)
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' = Graph (Maybe (a, Substitution a))
-> Maybe (Graph (a, Substitution a))
forall a. Ord a => Graph (Maybe a) -> Maybe (Graph a)
G.sequenceGraph (Graph (Maybe (a, Substitution a))
 -> Maybe (Graph (a, Substitution a)))
-> Graph (Maybe (a, Substitution a))
-> Maybe (Graph (a, Substitution a))
forall a b. (a -> b) -> a -> b
$ (Set a -> Maybe (a, Substitution a))
-> Graph (Set a) -> Graph (Maybe (a, Substitution a))
forall b a. Ord b => (a -> b) -> Graph a -> Graph b
G.map Set a -> Maybe (a, Substitution a)
unifySCC (Graph a -> Graph (Set a)
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 Set a -> [a]
forall a. Set a -> [a]
S.toList Set a
uatoms of
      []       -> String -> Maybe (a, Substitution a)
forall a. HasCallStack => String -> a
error String
"Impossible! unifySCC on the empty set"
      as :: [a]
as@(a
a:[a]
_) -> ((Substitution a -> a -> a) -> a -> Substitution a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Substitution a -> a -> a
forall b a. Subst b a => Substitution b -> a -> a
applySubst a
a (Substitution a -> a)
-> (Substitution a -> Substitution a)
-> Substitution a
-> (a, Substitution a)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Substitution a -> Substitution a
forall a. a -> a
id) (Substitution a -> (a, Substitution a))
-> Maybe (Substitution a) -> Maybe (a, Substitution a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Maybe (Substitution a)
genUnify [a]
as

------------------------------------------------------------
-- Steps 7 and 8: Constraint resolution
------------------------------------------------------------

-- | Rels stores the set of base types and variables related to a
--   given variable in the constraint graph (either predecessors or
--   successors, but not both).
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
(Int -> Rels -> ShowS)
-> (Rels -> String) -> ([Rels] -> ShowS) -> Show Rels
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
(Rels -> Rels -> Bool) -> (Rels -> Rels -> Bool) -> Eq Rels
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)

-- | A RelMap associates each variable to its sets of base type and
--   variable predecessors and successors in the constraint graph.
newtype RelMap = RelMap { RelMap -> Map (Name Type, Dir) Rels
unRelMap :: Map (Name Type, Dir) Rels}

instance Pretty RelMap where
  pretty :: RelMap -> Sem r Doc
pretty (RelMap Map (Name Type, Dir) Rels
rm) = [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat (((Rels, Name Type, Rels) -> Sem r Doc)
-> [(Rels, Name Type, Rels)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Rels, Name Type, Rels) -> Sem r Doc
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Reader PA) r, Member LFresh r, Pretty t) =>
(Rels, t, Rels) -> Sem r Doc
prettyVar [(Rels, Name Type, Rels)]
byVar)
    where
      vars :: Set (Name Type)
vars = ((Name Type, Dir) -> Name Type)
-> Set (Name Type, Dir) -> Set (Name Type)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (Name Type, Dir) -> Name Type
forall a b. (a, b) -> a
fst (Map (Name Type, Dir) Rels -> Set (Name Type, Dir)
forall k a. Map k a -> Set k
M.keysSet Map (Name Type, Dir) Rels
rm)
      byVar :: [(Rels, Name Type, Rels)]
byVar = (Name Type -> (Rels, Name Type, Rels))
-> [Name Type] -> [(Rels, Name Type, Rels)]
forall a b. (a -> b) -> [a] -> [b]
map (\Name Type
x -> (Map (Name Type, Dir) Rels
rmMap (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
forall k a. Ord k => Map k a -> k -> a
!(Name Type
x,Dir
SubTy), Name Type
x, Map (Name Type, Dir) Rels
rmMap (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
forall k a. Ord k => Map k a -> k -> a
!(Name Type
x,Dir
SuperTy))) (Set (Name Type) -> [Name Type]
forall a. Set a -> [a]
S.toList Set (Name Type)
vars)

      prettyVar :: (Rels, t, Rels) -> Sem r Doc
prettyVar (Rels
subs, t
x, Rels
sups) = [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Rels -> Sem r Doc
forall (r :: [(* -> *) -> * -> *]).
(Member (Reader PA) r, Member LFresh r) =>
Rels -> Sem r Doc
prettyRel Rels
subs, Sem r Doc
"<:", t -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty t
x, Sem r Doc
"<:", Rels -> Sem r Doc
forall (r :: [(* -> *) -> * -> *]).
(Member (Reader PA) r, Member LFresh r) =>
Rels -> Sem r Doc
prettyRel Rels
sups]
      prettyRel :: Rels -> Sem r Doc
prettyRel Rels
rs = Set BaseTy -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (Rels -> Set BaseTy
baseRels Rels
rs) Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc
", " Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Set (Name Type) -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (Rels -> Set (Name Type)
varRels Rels
rs)

-- | Modify a @RelMap@ to record the fact that we have solved for a
--   type variable.  In particular, delete the variable from the
--   @RelMap@ as a key, and also update the relative sets of every
--   other variable to remove this variable and add the base type we
--   chose for it.
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
  (Map (Name Type, Dir) Rels -> RelMap)
-> (RelMap -> Map (Name Type, Dir) Rels) -> RelMap -> RelMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name Type, Dir)
-> Map (Name Type, Dir) Rels -> Map (Name Type, Dir) Rels
forall k a. Ord k => k -> Map k a -> Map k a
M.delete (Name Type
x,Dir
SuperTy)
  (Map (Name Type, Dir) Rels -> Map (Name Type, Dir) Rels)
-> (RelMap -> Map (Name Type, Dir) Rels)
-> RelMap
-> Map (Name Type, Dir) Rels
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name Type, Dir)
-> Map (Name Type, Dir) Rels -> Map (Name Type, Dir) Rels
forall k a. Ord k => k -> Map k a -> Map k a
M.delete (Name Type
x,Dir
SubTy)
  (Map (Name Type, Dir) Rels -> Map (Name Type, Dir) Rels)
-> (RelMap -> Map (Name Type, Dir) Rels)
-> RelMap
-> Map (Name Type, Dir) Rels
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rels -> Rels)
-> Map (Name Type, Dir) Rels -> Map (Name Type, Dir) Rels
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 Name Type -> Set (Name Type) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set (Name Type)
v then Set BaseTy -> Set (Name Type) -> Rels
Rels (BaseTy -> Set BaseTy -> Set BaseTy
forall a. Ord a => a -> Set a -> Set a
S.insert BaseTy
ty Set BaseTy
b) (Name Type -> Set (Name Type) -> Set (Name Type)
forall a. Ord a => a -> Set a -> Set a
S.delete Name Type
x Set (Name Type)
v) else Rels
r)
  (Map (Name Type, Dir) Rels -> Map (Name Type, Dir) Rels)
-> (RelMap -> Map (Name Type, Dir) Rels)
-> RelMap
-> Map (Name Type, Dir) Rels
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelMap -> Map (Name Type, Dir) Rels
unRelMap

-- | Essentially dirtypesBySort vm rm dir t s x finds all the
--   dir-types (sub- or super-) of t which have sort s, relative to
--   the variables in x.  This is \overbar{T}_S^X (resp. \underbar...)
--   from Traytel et al.
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

    -- Keep only those supertypes t' of t
  = [BaseTy] -> (BaseTy -> Bool) -> [BaseTy]
forall a. [a] -> (a -> Bool) -> [a]
keep (Dir -> BaseTy -> [BaseTy]
dirtypes Dir
dir BaseTy
t) ((BaseTy -> Bool) -> [BaseTy]) -> (BaseTy -> Bool) -> [BaseTy]
forall a b. (a -> b) -> a -> b
$ \BaseTy
t' ->
      -- which have the right sort, and such that
      BaseTy -> Sort -> Bool
hasSort BaseTy
t' Sort
s Bool -> Bool -> Bool
&&

      -- for all variables beta \in x,
      Set (Name Type) -> (Name Type -> Bool) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> (a -> Bool) -> Bool
forAll Set (Name Type)
x (\Name Type
beta ->

        -- there is at least one type t'' which is a subtype of t'
        -- which would be a valid solution for beta, that is,
        [BaseTy] -> (BaseTy -> Bool) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> (a -> Bool) -> Bool
exists (Dir -> BaseTy -> [BaseTy]
dirtypes (Dir -> Dir
other Dir
dir) BaseTy
t') ((BaseTy -> Bool) -> Bool) -> (BaseTy -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \BaseTy
t'' ->

          -- t'' has the sort beta is supposed to have, and
          BaseTy -> Sort -> Bool
hasSort BaseTy
t'' (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
beta) Bool -> Bool -> Bool
&&

          -- t'' is a supertype of every base type predecessor of beta.
          Set BaseTy -> (BaseTy -> Bool) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> (a -> Bool) -> Bool
forAll (Rels -> Set BaseTy
baseRels (String -> Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
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''))

    -- The above comments are written assuming dir = Super; of course,
    -- if dir = Sub then just swap "super" and "sub" everywhere.

  where
    forAll, exists :: Foldable t => t a -> (a -> Bool) -> Bool
    forAll :: t a -> (a -> Bool) -> Bool
forAll = ((a -> Bool) -> t a -> Bool) -> t a -> (a -> Bool) -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> Bool) -> t a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
    exists :: t a -> (a -> Bool) -> Bool
exists = ((a -> Bool) -> t a -> Bool) -> t a -> (a -> Bool) -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> Bool) -> t a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any
    keep :: [a] -> (a -> Bool) -> [a]
keep   = ((a -> Bool) -> [a] -> [a]) -> [a] -> (a -> Bool) -> [a]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter

-- | Sort-aware infimum or supremum.
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 -> (BaseTy -> Bool) -> [BaseTy] -> Maybe BaseTy
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\BaseTy
lim -> (BaseTy -> Bool) -> [BaseTy] -> Bool
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)
  ([BaseTy] -> Maybe BaseTy)
-> ([BaseTy] -> [BaseTy]) -> [BaseTy] -> Maybe BaseTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[BaseTy]] -> [BaseTy]
isects
  ([[BaseTy]] -> [BaseTy])
-> ([BaseTy] -> [[BaseTy]]) -> [BaseTy] -> [BaseTy]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BaseTy -> [BaseTy]) -> [BaseTy] -> [[BaseTy]]
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)
  ([BaseTy] -> Maybe BaseTy) -> [BaseTy] -> Maybe BaseTy
forall a b. (a -> b) -> a -> b
$ [BaseTy]
ts
  where
    isects :: [[BaseTy]] -> [BaseTy]
isects = ([BaseTy] -> [BaseTy] -> [BaseTy]) -> [[BaseTy]] -> [BaseTy]
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 [BaseTy] -> [BaseTy] -> [BaseTy]
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

-- | From the constraint graph, build the sets of sub- and super- base
--   types of each type variable, as well as the sets of sub- and
--   supertype variables.  For each type variable x in turn, try to
--   find a common supertype of its base subtypes which is consistent
--   with the sort of x and with the sorts of all its sub-variables,
--   as well as symmetrically a common subtype of its supertypes, etc.
--   Assign x one of the two: if it has only successors, assign it
--   their inf; otherwise, assign it the sup of its predecessors.  If
--   it has both, we have a choice of whether to assign it the sup of
--   predecessors or inf of successors; both lead to a sound &
--   complete algorithm.  We choose to assign it the sup of its
--   predecessors in this case, since it seems nice to default to
--   "simpler" types lower down in the subtyping chain.
solveGraph
  :: Members '[Fresh, Error SolveError, Output Message] r
  => TyVarInfoMap -> Graph UAtom -> Sem r S
solveGraph :: TyVarInfoMap -> Graph UAtom -> Sem r S
solveGraph TyVarInfoMap
vm Graph UAtom
g = Substitution Atom -> S
atomToTypeSubst (Substitution Atom -> S)
-> (Substitution BaseTy -> Substitution Atom)
-> Substitution BaseTy
-> S
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution BaseTy -> Substitution Atom
unifyWCC (Substitution BaseTy -> S)
-> Sem r (Substitution BaseTy) -> Sem r S
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RelMap -> Sem r (Substitution BaseTy)
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output Message] r =>
RelMap -> Sem r (Substitution BaseTy)
go RelMap
topRelMap
  where
    unifyWCC :: Substitution BaseTy -> Substitution Atom
    unifyWCC :: Substitution BaseTy -> Substitution Atom
unifyWCC Substitution BaseTy
s = [Substitution Atom] -> Substitution Atom
forall a (t :: * -> *).
(Subst a a, Foldable t) =>
t (Substitution a) -> Substitution a
compose ((Set (Name Type) -> Substitution Atom)
-> [Set (Name Type)] -> [Substitution Atom]
forall a b. (a -> b) -> [a] -> [b]
map Set (Name Type) -> Substitution Atom
mkEquateSubst [Set (Name Type)]
wccVarGroups) Substitution Atom -> Substitution Atom -> Substitution Atom
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ (BaseTy -> Atom) -> Substitution BaseTy -> Substitution Atom
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  = (Set UAtom -> Set (Name Type)) -> [Set UAtom] -> [Set (Name Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((UAtom -> Name Type) -> Set UAtom -> Set (Name Type)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map UAtom -> Name Type
getVar) ([Set UAtom] -> [Set (Name Type)])
-> ([Set UAtom] -> [Set UAtom]) -> [Set UAtom] -> [Set (Name Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set UAtom -> Bool) -> [Set UAtom] -> [Set UAtom]
forall a. (a -> Bool) -> [a] -> [a]
filter ((UAtom -> Bool) -> Set UAtom -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all UAtom -> Bool
uisVar) ([Set UAtom] -> [Set UAtom])
-> ([Set UAtom] -> [Set UAtom]) -> [Set UAtom] -> [Set UAtom]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution BaseTy -> [Set UAtom] -> [Set UAtom]
forall b a. Subst b a => Substitution b -> a -> a
applySubst Substitution BaseTy
s ([Set UAtom] -> [Set (Name Type)])
-> [Set UAtom] -> [Set (Name Type)]
forall a b. (a -> b) -> a -> b
$ Graph UAtom -> [Set UAtom]
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) = String -> Name Type
forall a. HasCallStack => String -> a
error
          (String -> Name Type) -> String -> Name Type
forall a b. (a -> b) -> a -> b
$ String
"Impossible! Base type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BaseTy -> String
forall a. Show a => a -> String
show BaseTy
b String -> ShowS
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 ([Name Type] -> Substitution Atom)
-> (Set (Name Type) -> [Name Type])
-> Set (Name Type)
-> Substitution Atom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Name Type) -> [Name Type]
forall a. Set a -> [a]
S.toList

        mkEquations :: [Name Type] -> Substitution Atom
mkEquations (Name Type
a:[Name Type]
as) = [(Name Atom, Atom)] -> Substitution Atom
forall a. [(Name a, a)] -> Substitution a
Subst.fromList ([(Name Atom, Atom)] -> Substitution Atom)
-> ([Name Type] -> [(Name Atom, Atom)])
-> [Name Type]
-> Substitution Atom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name Type -> (Name Atom, Atom))
-> [Name Type] -> [(Name Atom, Atom)]
forall a b. (a -> b) -> [a] -> [b]
map (\Name Type
v -> (Name Type -> Name Atom
coerce Name Type
v, Var -> Atom
AVar (Name Type -> Var
U Name Type
a))) ([Name Type] -> Substitution Atom)
-> [Name Type] -> Substitution Atom
forall a b. (a -> b) -> a -> b
$ [Name Type]
as
        mkEquations []     = String -> Substitution Atom
forall a. HasCallStack => String -> a
error String
"Impossible! Empty set of names in mkEquateSubst"

            -- After picking concrete base types for all the type
            -- variables we can, the only thing possibly remaining in
            -- the graph are components containing only type variables
            -- and no base types.  It is sound, and simplifies the
            -- generated types considerably, to simply unify any type
            -- variables which are related by subtyping constraints.
            -- That is, we collect all the type variables in each
            -- weakly connected component and unify them.
            --
            -- As an example where this final step makes a difference,
            -- consider a term like @\x. (\y.y) x@.  A fresh type
            -- variable is generated for the type of @x@, and another
            -- for the type of @y@; the application of @(\y.y)@ to @x@
            -- induces a subtyping constraint between the two type
            -- variables.  The most general type would be something
            -- like @forall a b. (a <: b) => a -> b@, but we want to
            -- avoid generating unnecessary subtyping constraints (the
            -- type system might not even support subtyping qualifiers
            -- like this).  Instead, we unify the two type variables
            -- and the resulting type is @forall a. a -> a@.

    -- Get the successor and predecessor sets for all the type variables.
    topRelMap :: RelMap
    topRelMap :: RelMap
topRelMap
      = Map (Name Type, Dir) Rels -> RelMap
RelMap
      (Map (Name Type, Dir) Rels -> RelMap)
-> (Map (Name Type, Dir) (Set UAtom) -> Map (Name Type, Dir) Rels)
-> Map (Name Type, Dir) (Set UAtom)
-> RelMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set UAtom -> Rels)
-> Map (Name Type, Dir) (Set UAtom) -> Map (Name Type, Dir) Rels
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((Set BaseTy -> Set (Name Type) -> Rels)
-> (Set BaseTy, Set (Name Type)) -> Rels
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Set BaseTy -> Set (Name Type) -> Rels
Rels ((Set BaseTy, Set (Name Type)) -> Rels)
-> (Set UAtom -> (Set BaseTy, Set (Name Type)))
-> Set UAtom
-> Rels
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([BaseTy] -> Set BaseTy
forall a. Eq a => [a] -> Set a
S.fromAscList ([BaseTy] -> Set BaseTy)
-> ([Name Type] -> Set (Name Type))
-> ([BaseTy], [Name Type])
-> (Set BaseTy, Set (Name Type))
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [Name Type] -> Set (Name Type)
forall a. Eq a => [a] -> Set a
S.fromAscList)
               (([BaseTy], [Name Type]) -> (Set BaseTy, Set (Name Type)))
-> (Set UAtom -> ([BaseTy], [Name Type]))
-> Set UAtom
-> (Set BaseTy, Set (Name Type))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Either BaseTy (Name Type)] -> ([BaseTy], [Name Type])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either BaseTy (Name Type)] -> ([BaseTy], [Name Type]))
-> (Set UAtom -> [Either BaseTy (Name Type)])
-> Set UAtom
-> ([BaseTy], [Name Type])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UAtom -> Either BaseTy (Name Type))
-> [UAtom] -> [Either BaseTy (Name Type)]
forall a b. (a -> b) -> [a] -> [b]
map UAtom -> Either BaseTy (Name Type)
uatomToEither ([UAtom] -> [Either BaseTy (Name Type)])
-> (Set UAtom -> [UAtom])
-> Set UAtom
-> [Either BaseTy (Name Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set UAtom -> [UAtom]
forall a. Set a -> [a]
S.toList)
      (Map (Name Type, Dir) (Set UAtom) -> RelMap)
-> Map (Name Type, Dir) (Set UAtom) -> RelMap
forall a b. (a -> b) -> a -> b
$ (Name Type -> (Name Type, Dir))
-> Map (Name Type) (Set UAtom) -> Map (Name Type, Dir) (Set UAtom)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys (,Dir
SuperTy) Map (Name Type) (Set UAtom)
subMap Map (Name Type, Dir) (Set UAtom)
-> Map (Name Type, Dir) (Set UAtom)
-> Map (Name Type, Dir) (Set UAtom)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` (Name Type -> (Name Type, Dir))
-> Map (Name Type) (Set UAtom) -> Map (Name Type, Dir) (Set UAtom)
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 (Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom))
-> (Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom))
-> (Map UAtom (Set UAtom), Map UAtom (Set UAtom))
-> (Map (Name Type) (Set UAtom), Map (Name Type) (Set UAtom))
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) ((Map UAtom (Set UAtom), Map UAtom (Set UAtom))
 -> (Map (Name Type) (Set UAtom), Map (Name Type) (Set UAtom)))
-> (Map UAtom (Set UAtom), Map UAtom (Set UAtom))
-> (Map (Name Type) (Set UAtom), Map (Name Type) (Set UAtom))
forall a b. (a -> b) -> a -> b
$ Graph UAtom -> (Map UAtom (Set UAtom), Map UAtom (Set UAtom))
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 = (UAtom -> Name Type)
-> Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys UAtom -> Name Type
fromVar (Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom))
-> (Map UAtom (Set UAtom) -> Map UAtom (Set UAtom))
-> Map UAtom (Set UAtom)
-> Map (Name Type) (Set UAtom)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UAtom -> Set UAtom -> Bool)
-> Map UAtom (Set UAtom) -> Map UAtom (Set UAtom)
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
_      = String -> Name Type
forall a. HasCallStack => String -> a
error String
"Impossible! UB but uisVar."

    go
      :: Members '[Fresh, Error SolveError, Output Message] r
      => RelMap -> Sem r (Substitution BaseTy)
    go :: RelMap -> Sem r (Substitution BaseTy)
go relMap :: RelMap
relMap@(RelMap Map (Name Type, Dir) Rels
rm) = RelMap -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty RelMap
relMap Sem r ()
-> Sem r (Substitution BaseTy) -> Sem r (Substitution BaseTy)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> case [Name Type]
as of

      -- No variables left that have base type constraints.
      []    -> Substitution BaseTy -> Sem r (Substitution BaseTy)
forall (m :: * -> *) a. Monad m => a -> m a
return Substitution BaseTy
forall a. Substitution a
idS

      -- Solve one variable at a time.  See below.
      (Name Type
a:[Name Type]
_) -> do
        Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"Solving for" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Name Type -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]). Pretty t => t -> Sem r Doc
pretty' Name Type
a
        case Name Type -> Maybe (Substitution BaseTy)
solveVar Name Type
a of
          Maybe (Substitution BaseTy)
Nothing       -> do
            Sem r Doc -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"Couldn't solve for" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Name Type -> Sem r Doc
forall t (r :: [(* -> *) -> * -> *]). Pretty t => t -> Sem r Doc
pretty' Name Type
a
            SolveError -> Sem r (Substitution BaseTy)
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify

          -- If we solved for a, delete it from the maps, apply the
          -- resulting substitution to the remainder (updating the
          -- relMap appropriately), and recurse.  The substitution we
          -- want will be the composition of the substitution for a
          -- with the substitution generated by the recursive call.
          --
          -- Note we don't need to delete a from the TyVarInfoMap; we
          -- never use the set of keys from the TyVarInfoMap for
          -- anything (indeed, some variables might not be keys if
          -- they have an empty sort), so it doesn't matter if old
          -- variables hang around in it.
          Just Substitution BaseTy
s -> do
            Substitution BaseTy -> Sem r ()
forall (r :: [(* -> *) -> * -> *]) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
debugPretty Substitution BaseTy
s
            (Substitution BaseTy -> Substitution BaseTy -> Substitution BaseTy
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ Substitution BaseTy
s) (Substitution BaseTy -> Substitution BaseTy)
-> Sem r (Substitution BaseTy) -> Sem r (Substitution BaseTy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RelMap -> Sem r (Substitution BaseTy)
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output Message] r =>
RelMap -> Sem r (Substitution BaseTy)
go (Name Type -> BaseTy -> RelMap -> RelMap
substRel Name Type
a (Maybe BaseTy -> BaseTy
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe BaseTy -> BaseTy) -> Maybe BaseTy -> BaseTy
forall a b. (a -> b) -> a -> b
$ Name BaseTy -> Substitution BaseTy -> Maybe BaseTy
forall a. Name a -> Substitution a -> Maybe a
Subst.lookup (Name Type -> Name BaseTy
coerce Name Type
a) Substitution BaseTy
s) RelMap
relMap)

      where
        -- NOTE we can't solve a bunch in parallel!  Might end up
        -- assigning them conflicting solutions if some depend on
        -- others.  For example, consider the situation
        --
        --            Z
        --            |
        --            a3
        --           /  \
        --          a1   N
        --
        -- If we try to solve in parallel we will end up assigning a1
        -- -> Z (since it only has base types as an upper bound) and
        -- a3 -> N (since it has both upper and lower bounds, and by
        -- default we pick the lower bound), but this is wrong since
        -- we should have a1 < a3.
        --
        -- If instead we solve them one at a time, we could e.g. first
        -- solve a1 -> Z, and then we would find a3 -> Z as well.
        -- Alternately, if we first solve a3 -> N then we will have a1
        -- -> N as well.  Both are acceptable.
        --
        -- In fact, this exact graph comes from (^x.x+1) which was
        -- erroneously being inferred to have type Z -> N when I first
        -- wrote the code.

        -- Get only the variables we can solve on this pass, which
        -- have base types in their predecessor or successor set.  If
        -- there are no such variables, then start picking any
        -- remaining variables with a sort and pick types for them
        -- (disco doesn't have qualified polymorphism so we can't just
        -- leave them).
        asBase :: [Name Type]
asBase
          = ((Name Type, Dir) -> Name Type)
-> [(Name Type, Dir)] -> [Name Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type, Dir) -> Name Type
forall a b. (a, b) -> a
fst
          ([(Name Type, Dir)] -> [Name Type])
-> ([(Name Type, Dir)] -> [(Name Type, Dir)])
-> [(Name Type, Dir)]
-> [Name Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name Type, Dir) -> Bool)
-> [(Name Type, Dir)] -> [(Name Type, Dir)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Name Type, Dir) -> Bool) -> (Name Type, Dir) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set BaseTy -> Bool
forall a. Set a -> Bool
S.null (Set BaseTy -> Bool)
-> ((Name Type, Dir) -> Set BaseTy) -> (Name Type, Dir) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rels -> Set BaseTy
baseRels (Rels -> Set BaseTy)
-> ((Name Type, Dir) -> Rels) -> (Name Type, Dir) -> Set BaseTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
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)
          ([(Name Type, Dir)] -> [Name Type])
-> [(Name Type, Dir)] -> [Name Type]
forall a b. (a -> b) -> a -> b
$ Map (Name Type, Dir) Rels -> [(Name Type, Dir)]
forall k a. Map k a -> [k]
M.keys Map (Name Type, Dir) Rels
rm
        as :: [Name Type]
as = case [Name Type]
asBase of
          [] -> (Name Type -> Bool) -> [Name Type] -> [Name Type]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
/= Sort
topSort) (Sort -> Bool) -> (Name Type -> Sort) -> Name Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm) ([Name Type] -> [Name Type])
-> ([(Name Type, Dir)] -> [Name Type])
-> [(Name Type, Dir)]
-> [Name Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name Type, Dir) -> Name Type)
-> [(Name Type, Dir)] -> [Name Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type, Dir) -> Name Type
forall a b. (a, b) -> a
fst ([(Name Type, Dir)] -> [Name Type])
-> [(Name Type, Dir)] -> [Name Type]
forall a b. (a -> b) -> a -> b
$ Map (Name Type, Dir) Rels -> [(Name Type, Dir)]
forall k a. Map k a -> [k]
M.keys Map (Name Type, Dir) Rels
rm
          [Name Type]
_  -> [Name Type]
asBase

        -- Solve for a variable, failing if it has no solution, otherwise returning
        -- a substitution for it.
        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)) ((Name Type, Dir), (Name Type, Dir))
-> (((Name Type, Dir), (Name Type, Dir)) -> ([BaseTy], [BaseTy]))
-> ([BaseTy], [BaseTy])
forall a b. a -> (a -> b) -> b
& ASetter
  ((Name Type, Dir), (Name Type, Dir))
  ([BaseTy], [BaseTy])
  (Name Type, Dir)
  [BaseTy]
-> ((Name Type, Dir) -> [BaseTy])
-> ((Name Type, Dir), (Name Type, Dir))
-> ([BaseTy], [BaseTy])
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  ((Name Type, Dir), (Name Type, Dir))
  ([BaseTy], [BaseTy])
  (Name Type, Dir)
  [BaseTy]
forall (r :: * -> * -> *) a b.
Bitraversable r =>
Traversal (r a a) (r b b) a b
both (Set BaseTy -> [BaseTy]
forall a. Set a -> [a]
S.toList (Set BaseTy -> [BaseTy])
-> ((Name Type, Dir) -> Set BaseTy) -> (Name Type, Dir) -> [BaseTy]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rels -> Set BaseTy
baseRels (Rels -> Set BaseTy)
-> ((Name Type, Dir) -> Rels) -> (Name Type, Dir) -> Set BaseTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
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
            -- No sub- or supertypes; the only way this can happen is
            -- if it has a nontrivial sort.
            --
            -- Traytel et al. don't seem to have a rule saying what to
            -- do in this case (see Fig. 16 on p. 16 of their long
            -- version).  We used to just pick a type that inhabits
            -- the sort, but this is wrong; see
            -- https://github.com/disco-lang/disco/issues/192.
            --
            -- For now, let's assume that any situation in which we
            -- have no base sub- or supertypes but we do have
            -- nontrivial sorts means that we are dealing with numeric
            -- types; so we can just call N a base subtype and go from there.

            ([], []) ->
              -- Debug.trace (show v ++ " has no sub- or supertypes.  Assuming N as a subtype.")
              (Name Type -> Name BaseTy
coerce Name Type
v Name BaseTy -> BaseTy -> Substitution BaseTy
forall a. Name a -> a -> Substitution a
|->) (BaseTy -> Substitution BaseTy)
-> Maybe BaseTy -> Maybe (Substitution BaseTy)
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 (String -> Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
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)))

            -- Only supertypes.  Just assign a to their inf, if one exists.
            ([BaseTy]
bsupers, []) ->
              -- Debug.trace (show v ++ " has only supertypes (" ++ show bsupers ++ ")") $
              (Name Type -> Name BaseTy
coerce Name Type
v Name BaseTy -> BaseTy -> Substitution BaseTy
forall a. Name a -> a -> Substitution a
|->) (BaseTy -> Substitution BaseTy)
-> Maybe BaseTy -> Maybe (Substitution BaseTy)
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 (String -> Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
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)))

            -- Only subtypes.  Just assign a to their sup.
            ([], [BaseTy]
bsubs)   ->
              -- Debug.trace (show v ++ " has only subtypes (" ++ show bsubs ++ ")") $
              -- Debug.trace ("sortmap: " ++ show vm) $
              -- Debug.trace ("relmap: " ++ show relMap) $
              -- Debug.trace ("sort for " ++ show v ++ ": " ++ show (getSort vm v)) $
              -- Debug.trace ("relvars: " ++ show (varRels (relMap ! (v,SubTy)))) $
              (Name Type -> Name BaseTy
coerce Name Type
v Name BaseTy -> BaseTy -> Substitution BaseTy
forall a. Name a -> a -> Substitution a
|->) (BaseTy -> Substitution BaseTy)
-> Maybe BaseTy -> Maybe (Substitution BaseTy)
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 (String -> Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
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)))

            -- Both successors and predecessors.  Both must have a
            -- valid bound, and the bounds must not overlap.  Assign a
            -- to the sup of its predecessors.
            ([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 Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
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 Map (Name Type, Dir) Rels -> (Name Type, Dir) -> Rels
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  -> Substitution BaseTy -> Maybe (Substitution BaseTy)
forall a. a -> Maybe a
Just (Name Type -> Name BaseTy
coerce Name Type
v Name BaseTy -> BaseTy -> Substitution BaseTy
forall a. Name a -> a -> Substitution a
|-> BaseTy
lb)
                Bool
False -> Maybe (Substitution BaseTy)
forall a. Maybe a
Nothing