{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# 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 Control.Arrow ((&&&), (***))
import Control.Lens hiding (use, (%=), (.=))
import Control.Monad (forM, join, unless, zipWithM)
import Data.Bifunctor (first, second)
import Data.Coerce
import Data.Either (partitionEithers)
import Data.Foldable (Foldable (..))
import Data.List (
  find,
  intersect,
  partition,
 )
import Data.List.NonEmpty (NonEmpty (..))
import Data.List.NonEmpty qualified as NE
import Data.Map (Map, (!))
import Data.Map qualified as M
import Data.Maybe (
  fromJust,
  fromMaybe,
  mapMaybe,
 )
import Data.Monoid (First (..))
import Data.Semigroup (sconcat)
import Data.Set (Set)
import Data.Set qualified as S
import Data.Tuple
import Disco.Effects.Fresh
import Disco.Effects.State
import Disco.Messages
import Disco.Pretty hiding ((<>))
import Disco.Subst
import Disco.Subst qualified as Subst
import Disco.Typecheck.Constraints
import Disco.Typecheck.Graph (Graph)
import Disco.Typecheck.Graph qualified as G
import Disco.Typecheck.Unify
import Disco.Types
import Disco.Types.Qualifiers
import Disco.Types.Rules
import Disco.Util (partitionEithersNE)
import GHC.Generics (Generic)
import Polysemy
import Polysemy.Error
import Polysemy.Input
import Polysemy.Output
import Unbound.Generics.LocallyNameless (
  Alpha,
  Name,
  Subst,
  fv,
  name2Integer,
  string2Name,
  substs,
 )
import Prelude hiding (Foldable (..))

--------------------------------------------------
-- 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
$cshowsPrec :: Int -> SolveError -> ShowS
showsPrec :: Int -> SolveError -> ShowS
$cshow :: SolveError -> String
show :: SolveError -> String
$cshowList :: [SolveError] -> ShowS
showList :: [SolveError] -> ShowS
Show)

instance Semigroup SolveError where
  SolveError
e <> :: SolveError -> SolveError -> SolveError
<> SolveError
_ = SolveError
e

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

runSolve :: SolutionLimit -> Sem (State SolutionLimit ': Fresh ': Error SolveError ': r) a -> Sem r (Either SolveError a)
runSolve :: forall (r :: [(* -> *) -> * -> *]) a.
SolutionLimit
-> Sem (State SolutionLimit : Fresh : Error SolveError : r) a
-> Sem r (Either SolveError a)
runSolve SolutionLimit
lim = 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 (State SolutionLimit : Fresh : Error SolveError : r) a
    -> Sem (Error SolveError : r) a)
-> Sem (State SolutionLimit : 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 (Sem (Fresh : Error SolveError : r) a
 -> Sem (Error SolveError : r) a)
-> (Sem (State SolutionLimit : Fresh : Error SolveError : r) a
    -> Sem (Fresh : Error SolveError : r) a)
-> Sem (State SolutionLimit : Fresh : Error SolveError : r) a
-> Sem (Error SolveError : r) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolutionLimit
-> Sem (State SolutionLimit : Fresh : Error SolveError : r) a
-> Sem (Fresh : Error SolveError : r) a
forall s (r :: [(* -> *) -> * -> *]) a.
s -> Sem (State s : r) a -> Sem r a
evalState SolutionLimit
lim

-- | 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 => NonEmpty (Sem r a) -> Sem r (NonEmpty a)
filterErrors :: forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
NonEmpty (Sem r a) -> Sem r (NonEmpty a)
filterErrors NonEmpty (Sem r a)
ms = do
  NonEmpty (Either e a)
es <- (Sem r a -> Sem r (Either e a))
-> NonEmpty (Sem r a) -> Sem r (NonEmpty (Either e a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty 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 NonEmpty (Sem r a)
ms
  case NonEmpty (Either e a) -> Either (NonEmpty e) ([e], NonEmpty a)
forall a b.
NonEmpty (Either a b) -> Either (NonEmpty a) ([a], NonEmpty b)
partitionEithersNE NonEmpty (Either e a)
es of
    Left (e
e :| [e]
_) -> e -> Sem r (NonEmpty a)
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw e
e
    Right ([e]
_, NonEmpty a
as) -> NonEmpty a -> Sem r (NonEmpty a)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return NonEmpty a
as

--------------------------------------------------
-- Solution limits

-- | Max number of solutions to generate.
newtype SolutionLimit = SolutionLimit {SolutionLimit -> Int
getSolutionLimit :: Int}

-- | Register the fact that we found one solution, by decrementing the
--   solution limit.
countSolution :: Member (State SolutionLimit) r => Sem r ()
countSolution :: forall (r :: [(* -> *) -> * -> *]).
Member (State SolutionLimit) r =>
Sem r ()
countSolution = (SolutionLimit -> SolutionLimit) -> Sem r ()
forall s (r :: [(* -> *) -> * -> *]).
Member (State s) r =>
(s -> s) -> Sem r ()
modify (Int -> SolutionLimit
SolutionLimit (Int -> SolutionLimit)
-> (SolutionLimit -> Int) -> SolutionLimit -> SolutionLimit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
1 (Int -> Int) -> (SolutionLimit -> Int) -> SolutionLimit -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolutionLimit -> Int
getSolutionLimit)

-- | Run a subcomputation conditional on the solution limit still
--   being positive.  If the solution limit has reached zero, stop
--   early.
withSolutionLimit ::
  (Member (State SolutionLimit) r, Member (Output (Message ann)) r, Monoid a) =>
  Sem r a ->
  Sem r a
withSolutionLimit :: forall (r :: [(* -> *) -> * -> *]) ann a.
(Member (State SolutionLimit) r, Member (Output (Message ann)) r,
 Monoid a) =>
Sem r a -> Sem r a
withSolutionLimit Sem r a
m = do
  SolutionLimit Int
lim <- Sem r SolutionLimit
forall s (r :: [(* -> *) -> * -> *]). Member (State s) r => Sem r s
get
  case Int
lim of
    Int
0 -> do
      Sem r (Doc ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Reached solution limit, stopping early..."
      a -> Sem r a
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return a
forall a. Monoid a => a
mempty
    Int
_ -> Sem r a
m

--------------------------------------------------
-- 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
$cshowsPrec :: Int -> SimpleConstraint -> ShowS
showsPrec :: Int -> SimpleConstraint -> ShowS
$cshow :: SimpleConstraint -> String
show :: SimpleConstraint -> String
$cshowList :: [SimpleConstraint] -> ShowS
showList :: [SimpleConstraint] -> ShowS
Show, SimpleConstraint -> SimpleConstraint -> Bool
(SimpleConstraint -> SimpleConstraint -> Bool)
-> (SimpleConstraint -> SimpleConstraint -> Bool)
-> Eq SimpleConstraint
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SimpleConstraint -> SimpleConstraint -> Bool
== :: SimpleConstraint -> SimpleConstraint -> Bool
$c/= :: SimpleConstraint -> SimpleConstraint -> Bool
/= :: 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
$ccompare :: SimpleConstraint -> SimpleConstraint -> Ordering
compare :: SimpleConstraint -> SimpleConstraint -> Ordering
$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
>= :: SimpleConstraint -> SimpleConstraint -> Bool
$cmax :: SimpleConstraint -> SimpleConstraint -> SimpleConstraint
max :: SimpleConstraint -> SimpleConstraint -> SimpleConstraint
$cmin :: SimpleConstraint -> SimpleConstraint -> SimpleConstraint
min :: SimpleConstraint -> SimpleConstraint -> 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
$cfrom :: forall x. SimpleConstraint -> Rep SimpleConstraint x
from :: forall x. SimpleConstraint -> Rep SimpleConstraint x
$cto :: forall x. Rep SimpleConstraint x -> SimpleConstraint
to :: forall x. Rep SimpleConstraint x -> SimpleConstraint
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 -> Perm AnyName -> SimpleConstraint -> SimpleConstraint
AlphaCtx -> NamePatFind -> SimpleConstraint -> SimpleConstraint
AlphaCtx -> NthPatFind -> SimpleConstraint -> SimpleConstraint
AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Bool
AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Ordering
SimpleConstraint -> Bool
SimpleConstraint -> All
SimpleConstraint -> NamePatFind
SimpleConstraint -> NthPatFind
SimpleConstraint -> DisjointSet AnyName
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
$caeq' :: AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Bool
aeq' :: AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Bool
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> SimpleConstraint -> f SimpleConstraint
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> SimpleConstraint -> f SimpleConstraint
$cclose :: AlphaCtx -> NamePatFind -> SimpleConstraint -> SimpleConstraint
close :: AlphaCtx -> NamePatFind -> SimpleConstraint -> SimpleConstraint
$copen :: AlphaCtx -> NthPatFind -> SimpleConstraint -> SimpleConstraint
open :: AlphaCtx -> NthPatFind -> SimpleConstraint -> SimpleConstraint
$cisPat :: SimpleConstraint -> DisjointSet AnyName
isPat :: SimpleConstraint -> DisjointSet AnyName
$cisTerm :: SimpleConstraint -> All
isTerm :: SimpleConstraint -> All
$cisEmbed :: SimpleConstraint -> Bool
isEmbed :: SimpleConstraint -> Bool
$cnthPatFind :: SimpleConstraint -> NthPatFind
nthPatFind :: SimpleConstraint -> NthPatFind
$cnamePatFind :: SimpleConstraint -> NamePatFind
namePatFind :: SimpleConstraint -> NamePatFind
$cswaps' :: AlphaCtx -> Perm AnyName -> SimpleConstraint -> SimpleConstraint
swaps' :: AlphaCtx -> Perm AnyName -> SimpleConstraint -> SimpleConstraint
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> SimpleConstraint
-> (SimpleConstraint -> Perm AnyName -> m b)
-> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> SimpleConstraint
-> (SimpleConstraint -> Perm AnyName -> m b)
-> m b
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> SimpleConstraint -> m (SimpleConstraint, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> SimpleConstraint -> m (SimpleConstraint, Perm AnyName)
$cacompare' :: AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Ordering
acompare' :: AlphaCtx -> SimpleConstraint -> SimpleConstraint -> Ordering
Alpha, Subst Type)

instance Pretty SimpleConstraint where
  pretty :: forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
SimpleConstraint -> Sem r (Doc ann)
pretty = \case
    Type
ty1 :<: Type
ty2 -> Type -> Sem r (Doc ann)
forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty1 Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"<:" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Type -> Sem r (Doc ann)
forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty2
    Type
ty1 :=: Type
ty2 -> Type -> Sem r (Doc ann)
forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty1 Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"=" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Type -> Sem r (Doc ann)
forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
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
$cshowsPrec :: Int -> TyVarInfo -> ShowS
showsPrec :: Int -> TyVarInfo -> ShowS
$cshow :: TyVarInfo -> String
show :: TyVarInfo -> String
$cshowList :: [TyVarInfo] -> ShowS
showList :: [TyVarInfo] -> ShowS
Show)

makeLenses ''TyVarInfo

instance Pretty TyVarInfo where
  pretty :: forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
TyVarInfo -> Sem r (Doc ann)
pretty (TVI (First Maybe Ilk
ilk) Sort
s) = Sem r (Doc ann)
-> (Ilk -> Sem r (Doc ann)) -> Maybe Ilk -> Sem r (Doc ann)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Doc ann -> Sem r (Doc ann)
forall a. a -> Sem r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc ann
"?") Ilk -> Sem r (Doc ann)
forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
Ilk -> Sem r (Doc ann)
forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Maybe Ilk
ilk Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ann)
"%" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Semigroup a => a -> a -> a
<> Sort -> Sem r (Doc ann)
forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
Sort -> Sem r (Doc ann)
forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
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
$cshowsPrec :: Int -> TyVarInfoMap -> ShowS
showsPrec :: Int -> TyVarInfoMap -> ShowS
$cshow :: TyVarInfoMap -> String
show :: TyVarInfoMap -> String
$cshowList :: [TyVarInfoMap] -> ShowS
showList :: [TyVarInfoMap] -> ShowS
Show)

instance Pretty TyVarInfoMap where
  pretty :: forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
TyVarInfoMap -> Sem r (Doc ann)
pretty (VM Map (Name Type) TyVarInfo
m) = Map (Name Type) TyVarInfo -> Sem r (Doc ann)
forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
Map (Name Type) TyVarInfo -> Sem r (Doc ann)
forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
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 b a. (b -> a -> b) -> b -> [a] -> b
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 a b. Maybe a -> (a -> Maybe b) -> Maybe b
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 (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f b) -> p (Maybe a) (f (Maybe 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 :: forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
messg Map k a
m k
k = 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 ann), Input TyDefCtx, State SolutionLimit] r =>
  Constraint ->
  Sem r (NonEmpty S)
solveConstraint :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx,
    State SolutionLimit]
  r =>
Constraint -> Sem r (NonEmpty 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 ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"============================================================"
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Solving:"
  Constraint -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty Constraint
c

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

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

  -- Now try continuing with each set.
  NonEmpty (NonEmpty S) -> NonEmpty S
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty (NonEmpty S) -> NonEmpty S)
-> Sem r (NonEmpty (NonEmpty S)) -> Sem r (NonEmpty S)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Sem r (NonEmpty S)) -> Sem r (NonEmpty (NonEmpty S))
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
NonEmpty (Sem r a) -> Sem r (NonEmpty a)
filterErrors (((TyVarInfoMap, [SimpleConstraint]) -> Sem r (NonEmpty S))
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
-> NonEmpty (Sem r (NonEmpty S))
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map ((TyVarInfoMap -> [SimpleConstraint] -> Sem r (NonEmpty S))
-> (TyVarInfoMap, [SimpleConstraint]) -> Sem r (NonEmpty S)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TyVarInfoMap -> [SimpleConstraint] -> Sem r (NonEmpty S)
forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx,
    State SolutionLimit]
  r =>
TyVarInfoMap -> [SimpleConstraint] -> Sem r (NonEmpty S)
solveConstraintChoice) NonEmpty (TyVarInfoMap, [SimpleConstraint])
qcList)

solveConstraintChoice ::
  Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx, State SolutionLimit] r =>
  TyVarInfoMap ->
  [SimpleConstraint] ->
  Sem r (NonEmpty S)
solveConstraintChoice :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx,
    State SolutionLimit]
  r =>
TyVarInfoMap -> [SimpleConstraint] -> Sem r (NonEmpty S)
solveConstraintChoice TyVarInfoMap
quals [SimpleConstraint]
cs = do
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"solveConstraintChoice"

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

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

  -- 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 ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"------------------------------"
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Running simplifier..."

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

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

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

  Sem r (Doc ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"------------------------------"
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"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 b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (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 ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) 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 ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"------------------------------"
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Checking WCCs for skolems..."

  (Graph UAtom
g', S
theta_skolem) <- TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
checkSkolems TyVarInfoMap
vm Graph Atom
g
  S -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) 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 ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"------------------------------"
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Collapsing SCCs..."

  (Graph UAtom
g'', S
theta_cyc) <- 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 ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty Graph UAtom
g''
  S -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) 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 ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Old sort map:"
  TyVarInfoMap -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
vm

  let vm' :: TyVarInfoMap
vm' = ((Name Type, Type) -> TyVarInfoMap -> TyVarInfoMap)
-> TyVarInfoMap -> [(Name Type, Type)] -> TyVarInfoMap
forall a b. (a -> b -> b) -> b -> [a] -> b
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 ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Updated sort map:"
  TyVarInfoMap -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
vm

  Sem r (Doc ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"------------------------------"
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Checking edges between base types..."

  -- Step 6b. Collapsing SCCs can create some edges between base
  -- types.  Check that any such edges are consistent, then remove
  -- them, since they no longer give us any information about type
  -- variables.  See https://github.com/disco-lang/disco/issues/357.

  Graph UAtom
g''' <- Graph UAtom -> Sem r (Graph UAtom)
forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError] r =>
Graph UAtom -> Sem r (Graph UAtom)
checkBaseEdges Graph UAtom
g''

  -- 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 ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"------------------------------"
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Solving for type variables..."

  [S]
theta_sols <- TyVarInfoMap -> Graph UAtom -> Sem r [S]
forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Fresh, Error SolveError, Output (Message ann),
    State SolutionLimit]
  r =>
TyVarInfoMap -> Graph UAtom -> Sem r [S]
solveGraph TyVarInfoMap
vm' Graph UAtom
g'''
  case [S] -> Maybe (NonEmpty S)
forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty [S]
theta_sols of
    Maybe (NonEmpty S)
Nothing -> SolveError -> Sem r (NonEmpty S)
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
    Just NonEmpty S
theta_sols_NE -> do
      [S] -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty [S]
theta_sols

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

      let theta_finals :: NonEmpty S
theta_finals = (S -> S) -> NonEmpty S -> NonEmpty S
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map (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)) NonEmpty S
theta_sols_NE
      NonEmpty S -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty NonEmpty S
theta_finals

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

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

decomposeConstraint ::
  Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
  Constraint ->
  Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
decomposeConstraint :: forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
decomposeConstraint (CSub Type
t1 Type
t2) = NonEmpty (TyVarInfoMap, [SimpleConstraint])
-> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (NonEmpty (TyVarInfoMap, [SimpleConstraint])
 -> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint])))
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
-> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
forall a b. (a -> b) -> a -> b
$ (TyVarInfoMap, [SimpleConstraint])
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
forall a. a -> NonEmpty a
NE.singleton (TyVarInfoMap
forall a. Monoid a => a
mempty, [Type
t1 Type -> Type -> SimpleConstraint
:<: Type
t2])
decomposeConstraint (CEq Type
t1 Type
t2) = NonEmpty (TyVarInfoMap, [SimpleConstraint])
-> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (NonEmpty (TyVarInfoMap, [SimpleConstraint])
 -> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint])))
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
-> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
forall a b. (a -> b) -> a -> b
$ (TyVarInfoMap, [SimpleConstraint])
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
forall a. a -> NonEmpty a
NE.singleton (TyVarInfoMap
forall a. Monoid a => a
mempty, [Type
t1 Type -> Type -> SimpleConstraint
:=: Type
t2])
decomposeConstraint (CQual Qualifier
q Type
ty) = (TyVarInfoMap, [SimpleConstraint])
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
forall a. a -> NonEmpty a
NE.singleton ((TyVarInfoMap, [SimpleConstraint])
 -> NonEmpty (TyVarInfoMap, [SimpleConstraint]))
-> (TyVarInfoMap -> (TyVarInfoMap, [SimpleConstraint]))
-> TyVarInfoMap
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,[]) (TyVarInfoMap -> NonEmpty (TyVarInfoMap, [SimpleConstraint]))
-> Sem r TyVarInfoMap
-> Sem r (NonEmpty (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 NonEmpty Constraint
cs) = (NonEmpty (TyVarInfoMap, [SimpleConstraint])
 -> (TyVarInfoMap, [SimpleConstraint]))
-> NonEmpty (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NonEmpty (TyVarInfoMap, [SimpleConstraint])
-> (TyVarInfoMap, [SimpleConstraint])
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
 -> NonEmpty (TyVarInfoMap, [SimpleConstraint]))
-> (NonEmpty (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
    -> NonEmpty (NonEmpty (TyVarInfoMap, [SimpleConstraint])))
-> NonEmpty (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
-> NonEmpty (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => NonEmpty (m a) -> m (NonEmpty a)
sequence (NonEmpty (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
 -> NonEmpty (TyVarInfoMap, [SimpleConstraint]))
-> Sem r (NonEmpty (NonEmpty (TyVarInfoMap, [SimpleConstraint])))
-> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Constraint -> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint])))
-> NonEmpty Constraint
-> Sem r (NonEmpty (NonEmpty (TyVarInfoMap, [SimpleConstraint])))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM Constraint -> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
decomposeConstraint NonEmpty Constraint
cs
decomposeConstraint Constraint
CTrue = NonEmpty (TyVarInfoMap, [SimpleConstraint])
-> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (NonEmpty (TyVarInfoMap, [SimpleConstraint])
 -> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint])))
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
-> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
forall a b. (a -> b) -> a -> b
$ (TyVarInfoMap, [SimpleConstraint])
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
forall a. a -> NonEmpty a
NE.singleton (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]))
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map (((TyVarInfoMap, [SimpleConstraint])
  -> (TyVarInfoMap, [SimpleConstraint]))
 -> NonEmpty (TyVarInfoMap, [SimpleConstraint])
 -> NonEmpty (TyVarInfoMap, [SimpleConstraint]))
-> ([Name Type]
    -> (TyVarInfoMap, [SimpleConstraint])
    -> (TyVarInfoMap, [SimpleConstraint]))
-> [Name Type]
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVarInfoMap -> TyVarInfoMap)
-> (TyVarInfoMap, [SimpleConstraint])
-> (TyVarInfoMap, [SimpleConstraint])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((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 (NonEmpty (TyVarInfoMap, [SimpleConstraint])
 -> NonEmpty (TyVarInfoMap, [SimpleConstraint]))
-> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
-> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Constraint -> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r (NonEmpty (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 b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Name Type -> Type
TySkolem)
decomposeConstraint (COr NonEmpty Constraint
cs) = NonEmpty (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
-> NonEmpty (TyVarInfoMap, [SimpleConstraint])
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
 -> NonEmpty (TyVarInfoMap, [SimpleConstraint]))
-> Sem r (NonEmpty (NonEmpty (TyVarInfoMap, [SimpleConstraint])))
-> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint])))
-> Sem r (NonEmpty (NonEmpty (TyVarInfoMap, [SimpleConstraint])))
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
NonEmpty (Sem r a) -> Sem r (NonEmpty a)
filterErrors ((Constraint -> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint])))
-> NonEmpty Constraint
-> NonEmpty (Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint])))
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map Constraint -> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Constraint -> Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
decomposeConstraint NonEmpty Constraint
cs)

decomposeQual ::
  Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
  Type ->
  Qualifier ->
  Sem r TyVarInfoMap
decomposeQual :: forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Type -> Qualifier -> Sem r TyVarInfoMap
decomposeQual = 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 :: forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go Set (String, [Type], Qualifier)
_ (TyAtom Atom
a) Qualifier
q = 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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return TyVarInfoMap
forall a. Monoid a => a
mempty
      Bool
False -> do
        TyDefCtx
tyDefns <- 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 a. a -> Sem r a
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 :: forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError] r =>
Qualifier -> Atom -> Sem r TyVarInfoMap
checkQual Qualifier
q (AVar (U Name Type
v)) = TyVarInfoMap -> Sem r TyVarInfoMap
forall a. a -> Sem r a
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 a. a -> Sem r a
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 ann), Input TyDefCtx] r =>
  TyVarInfoMap ->
  [SimpleConstraint] ->
  Sem r (TyVarInfoMap, [(Atom, Atom)], S)
simplify :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
TyVarInfoMap
-> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)
simplify TyVarInfoMap
origVM [SimpleConstraint]
cs =
  (\(SS TyVarInfoMap
vm' [SimpleConstraint]
cs' S
s' Set SimpleConstraint
_) -> (TyVarInfoMap
vm', (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 ann (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError,
    Output (Message ann), Input TyDefCtx]
  r =>
Sem r ()
simplify')
 where
  fvNums :: Alpha a => [a] -> [Integer]
  fvNums :: forall a. Alpha a => [a] -> [Integer]
fvNums = (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 {a}. (Num a, Ord a) => [a] -> a
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 a. Ord a => [a] -> a
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
n1 Integer -> [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 :: [a] -> a
maximum0 [] = a
0
  maximum0 [a]
xs = [a] -> a
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [a]
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 ann), Input TyDefCtx] r =>
    Sem r ()
  simplify' :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError,
    Output (Message ann), Input TyDefCtx]
  r =>
Sem r ()
simplify' = do
    -- 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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Just SimpleConstraint
s -> do
        Sem r (Doc ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug (Sem r (Doc ann) -> Sem r ()) -> Sem r (Doc ann) -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Simplifying:" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> SimpleConstraint -> Sem r (Doc ann)
forall t (r :: [(* -> *) -> * -> *]) ann.
Pretty t =>
t -> Sem r (Doc ann)
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 ann (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError,
    Output (Message ann), 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 :: forall (r :: [(* -> *) -> * -> *]).
Members '[State SimplifyState, Fresh, Error SolveError] r =>
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 ([SimpleConstraint] -> f [SimpleConstraint])
-> SimplifyState -> f SimplifyState
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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SimpleConstraint
forall a. Maybe a
Nothing
      Just (SimpleConstraint
a, [SimpleConstraint]
as) -> do
        ([SimpleConstraint] -> f [SimpleConstraint])
-> SimplifyState -> f SimplifyState
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 a. a -> Sem r a
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 :: forall a. (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 b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (a
a a -> [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 :: forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
  r =>
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 (Set SimpleConstraint -> f (Set SimpleConstraint))
-> SimplifyState -> f SimplifyState
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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Bool
False -> do
        (Set SimpleConstraint -> f (Set SimpleConstraint))
-> SimplifyState -> f SimplifyState
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' :: forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
  r =>
SimpleConstraint -> Sem r ()
simplifyOne' (Type
ty1 :=: Type
ty2) = do
    TyDefCtx
tyDefns <- forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
    case TyDefCtx -> [(Type, Type)] -> Maybe S
unify TyDefCtx
tyDefns [(Type
ty1, Type
ty2)] of
      Maybe S
Nothing -> 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 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) ->
        ([SimpleConstraint] -> f [SimpleConstraint])
-> SimplifyState -> f SimplifyState
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 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) ->
        ([SimpleConstraint] -> f [SimpleConstraint])
-> SimplifyState -> f SimplifyState
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) =
    ([SimpleConstraint] -> f [SimpleConstraint])
-> SimplifyState -> f SimplifyState
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 =
        ([SimpleConstraint] -> f [SimpleConstraint])
-> SimplifyState -> f SimplifyState
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 a. a -> Sem r a
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 :: forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
  r =>
Name Type -> Con -> SimpleConstraint -> Sem r ()
expandStruct Name Type
a Con
c SimpleConstraint
con = do
    [Type]
as <- (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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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
    ([SimpleConstraint] -> f [SimpleConstraint])
-> SimplifyState -> f SimplifyState
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
con SimpleConstraint -> [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 :: forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
  r =>
S -> Sem r ()
extendSubst S
s' = do
    (S -> f S) -> SimplifyState -> f SimplifyState
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
@@)
    ([SimpleConstraint] -> f [SimpleConstraint])
-> SimplifyState -> f SimplifyState
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 :: forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
  r =>
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 (TyVarInfoMap -> f TyVarInfoMap)
-> SimplifyState -> f SimplifyState
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 b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (Type, a) -> f (Type, 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)
forall (f :: * -> *) a. Applicative f => (Type, f a) -> f (Type, 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 b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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.

    (TyVarInfoMap -> f TyVarInfoMap)
-> SimplifyState -> f SimplifyState
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 b a. (b -> a -> b) -> b -> Set a -> b
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 :: forall a. (Show a, Ord a) => 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [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
Traversal (a, a) (a, a) a a
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 ann), Input TyDefCtx] r =>
  TyVarInfoMap ->
  Graph Atom ->
  Sem r (Graph UAtom, S)
checkSkolems :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)
checkSkolems TyVarInfoMap
vm Graph Atom
graph = do
  let skolemWCCs :: [Set Atom]
      skolemWCCs :: [Set Atom]
skolemWCCs = (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 a. [a] -> 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 ann (r :: [(* -> *) -> * -> *]).
Members
  '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
graph 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 ann), Input TyDefCtx] r =>
    Graph Atom ->
    S ->
    [Set Atom] ->
    Sem r (Graph UAtom, S)
  unifyWCCs :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
g S
s [] = (Graph UAtom, S) -> Sem r (Graph UAtom, S)
forall a. a -> Sem r a
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 ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug (Sem r (Doc ann) -> Sem r ()) -> Sem r (Doc ann) -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Unifying" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> [Set Atom] -> Sem r (Doc ann)
forall t (r :: [(* -> *) -> * -> *]) ann.
Pretty t =>
t -> Sem r (Doc ann)
pretty' (Set Atom
u Set Atom -> [Set Atom] -> [Set Atom]
forall a. a -> [a] -> [a]
: [Set Atom]
us) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ann)
"..."

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

    let g' :: Graph Atom
g' = (Graph Atom -> Atom -> Graph Atom)
-> Graph Atom -> Set Atom -> Graph Atom
forall b a. (b -> a -> b) -> b -> Set a -> b
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 ann (r :: [(* -> *) -> * -> *]).
Members
  '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
g' (Substitution Atom -> S
atomToTypeSubst Substitution Atom
s' 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 :: forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError] r =>
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 :: forall a b (r :: [(* -> *) -> * -> *]).
(Subst a a, Ord a, Members '[Error SolveError] r) =>
(Substitution a -> Substitution b)
-> ([a] -> Maybe (Substitution a))
-> Graph a
-> Sem r (Graph a, Substitution b)
elimCyclesGen Substitution a -> Substitution b
genSubst [a] -> Maybe (Substitution a)
genUnify Graph a
g =
  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 b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
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 b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
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

------------------------------------------------------------
-- Step 6a: check base type edges
------------------------------------------------------------

isBaseEdge :: (UAtom, UAtom) -> Either (BaseTy, BaseTy) (UAtom, UAtom)
isBaseEdge :: (UAtom, UAtom) -> Either (BaseTy, BaseTy) (UAtom, UAtom)
isBaseEdge (UB BaseTy
b1, UB BaseTy
b2) = (BaseTy, BaseTy) -> Either (BaseTy, BaseTy) (UAtom, UAtom)
forall a b. a -> Either a b
Left (BaseTy
b1, BaseTy
b2)
isBaseEdge (UAtom, UAtom)
e = (UAtom, UAtom) -> Either (BaseTy, BaseTy) (UAtom, UAtom)
forall a b. b -> Either a b
Right (UAtom, UAtom)
e

checkBaseEdge :: Members '[Error SolveError] r => (BaseTy, BaseTy) -> Sem r ()
checkBaseEdge :: forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError] r =>
(BaseTy, BaseTy) -> Sem r ()
checkBaseEdge (BaseTy
b1, BaseTy
b2)
  | BaseTy -> BaseTy -> Bool
isSubB BaseTy
b1 BaseTy
b2 = () -> Sem r ()
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise = SolveError -> Sem r ()
forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify

checkBaseEdges :: Members '[Error SolveError] r => Graph UAtom -> Sem r (Graph UAtom)
checkBaseEdges :: forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError] r =>
Graph UAtom -> Sem r (Graph UAtom)
checkBaseEdges Graph UAtom
g = do
  let ([(BaseTy, BaseTy)]
baseEdges, [(UAtom, UAtom)]
varEdges) = [Either (BaseTy, BaseTy) (UAtom, UAtom)]
-> ([(BaseTy, BaseTy)], [(UAtom, UAtom)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either (BaseTy, BaseTy) (UAtom, UAtom)]
 -> ([(BaseTy, BaseTy)], [(UAtom, UAtom)]))
-> (Graph UAtom -> [Either (BaseTy, BaseTy) (UAtom, UAtom)])
-> Graph UAtom
-> ([(BaseTy, BaseTy)], [(UAtom, UAtom)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((UAtom, UAtom) -> Either (BaseTy, BaseTy) (UAtom, UAtom))
-> [(UAtom, UAtom)] -> [Either (BaseTy, BaseTy) (UAtom, UAtom)]
forall a b. (a -> b) -> [a] -> [b]
map (UAtom, UAtom) -> Either (BaseTy, BaseTy) (UAtom, UAtom)
isBaseEdge ([(UAtom, UAtom)] -> [Either (BaseTy, BaseTy) (UAtom, UAtom)])
-> (Graph UAtom -> [(UAtom, UAtom)])
-> Graph UAtom
-> [Either (BaseTy, BaseTy) (UAtom, UAtom)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (UAtom, UAtom) -> [(UAtom, UAtom)]
forall a. Set a -> [a]
S.toList (Set (UAtom, UAtom) -> [(UAtom, UAtom)])
-> (Graph UAtom -> Set (UAtom, UAtom))
-> Graph UAtom
-> [(UAtom, UAtom)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph UAtom -> Set (UAtom, UAtom)
forall a. Ord a => Graph a -> Set (a, a)
G.edges (Graph UAtom -> ([(BaseTy, BaseTy)], [(UAtom, UAtom)]))
-> Graph UAtom -> ([(BaseTy, BaseTy)], [(UAtom, UAtom)])
forall a b. (a -> b) -> a -> b
$ Graph UAtom
g
  ((BaseTy, BaseTy) -> Sem r ()) -> [(BaseTy, BaseTy)] -> Sem r ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (BaseTy, BaseTy) -> Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Members '[Error SolveError] r =>
(BaseTy, BaseTy) -> Sem r ()
checkBaseEdge [(BaseTy, BaseTy)]
baseEdges
  Graph UAtom -> Sem r (Graph UAtom)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Graph UAtom -> Sem r (Graph UAtom))
-> Graph UAtom -> Sem r (Graph UAtom)
forall a b. (a -> b) -> a -> b
$ Set UAtom -> Set (UAtom, UAtom) -> Graph UAtom
forall a. (Show a, Ord a) => Set a -> Set (a, a) -> Graph a
G.mkGraph (Graph UAtom -> Set UAtom
forall a. Graph a -> Set a
G.nodes Graph UAtom
g) ([(UAtom, UAtom)] -> Set (UAtom, UAtom)
forall a. Ord a => [a] -> Set a
S.fromList [(UAtom, UAtom)]
varEdges)

------------------------------------------------------------
-- 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
$cshowsPrec :: Int -> Rels -> ShowS
showsPrec :: Int -> Rels -> ShowS
$cshow :: Rels -> String
show :: Rels -> String
$cshowList :: [Rels] -> ShowS
showList :: [Rels] -> ShowS
Show, Rels -> Rels -> Bool
(Rels -> Rels -> Bool) -> (Rels -> Rels -> Bool) -> Eq Rels
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Rels -> Rels -> Bool
== :: Rels -> Rels -> Bool
$c/= :: Rels -> Rels -> Bool
/= :: 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}
  deriving (Int -> RelMap -> ShowS
[RelMap] -> ShowS
RelMap -> String
(Int -> RelMap -> ShowS)
-> (RelMap -> String) -> ([RelMap] -> ShowS) -> Show RelMap
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RelMap -> ShowS
showsPrec :: Int -> RelMap -> ShowS
$cshow :: RelMap -> String
show :: RelMap -> String
$cshowList :: [RelMap] -> ShowS
showList :: [RelMap] -> ShowS
Show)

instance Pretty RelMap where
  pretty :: forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
RelMap -> Sem r (Doc ann)
pretty (RelMap Map (Name Type, Dir) Rels
rm) = [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat (((Rels, Name Type, Rels) -> Sem r (Doc ann))
-> [(Rels, Name Type, Rels)] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map (Rels, Name Type, Rels) -> Sem r (Doc ann)
forall {r :: [(* -> *) -> * -> *]} {t} {ann}.
(Member (Reader PA) r, Member LFresh r, Pretty t) =>
(Rels, t, Rels) -> Sem r (Doc ann)
prettyVar [(Rels, Name Type, Rels)]
byVar)
   where
    vars :: Set (Name Type)
vars = ((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
rm Map (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
rm Map (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 ann)
prettyVar (Rels
subs, t
x, Rels
sups) = [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Rels -> Sem r (Doc ann)
forall {r :: [(* -> *) -> * -> *]} {ann}.
(Member (Reader PA) r, Member LFresh r) =>
Rels -> Sem r (Doc ann)
prettyRel Rels
subs, Sem r (Doc ann)
"<:", t -> Sem r (Doc ann)
forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
t -> Sem r (Doc ann)
forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty t
x, Sem r (Doc ann)
"<:", Rels -> Sem r (Doc ann)
forall {r :: [(* -> *) -> * -> *]} {ann}.
(Member (Reader PA) r, Member LFresh r) =>
Rels -> Sem r (Doc ann)
prettyRel Rels
sups]
    prettyRel :: Rels -> Sem r (Doc ann)
prettyRel Rels
rs = Set BaseTy -> Sem r (Doc ann)
forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
Set BaseTy -> Sem r (Doc ann)
forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty (Rels -> Set BaseTy
baseRels Rels
rs) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ann)
", " Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Semigroup a => a -> a -> a
<> Set (Name Type) -> Sem r (Doc ann)
forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
Set (Name Type) -> Sem r (Doc ann)
forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
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'')
        )
 where
  -- The above comments are written assuming dir = Super; of course,
  -- if dir = Sub then just swap "super" and "sub" everywhere.

  forAll, exists :: Foldable t => t a -> (a -> Bool) -> Bool
  forAll :: forall (t :: * -> *) a. Foldable t => 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 :: forall (t :: * -> *) a. Foldable t => 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 a. (a -> a -> a) -> [a] -> a
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

allBySort :: TyVarInfoMap -> RelMap -> Dir -> [BaseTy] -> Sort -> Set (Name Type) -> Set BaseTy
allBySort :: TyVarInfoMap
-> RelMap
-> Dir
-> [BaseTy]
-> Sort
-> Set (Name Type)
-> Set BaseTy
allBySort TyVarInfoMap
vm RelMap
rm Dir
dir [BaseTy]
ts Sort
s Set (Name Type)
x =
  [Set BaseTy] -> Set BaseTy
isects
    ([Set BaseTy] -> Set BaseTy)
-> ([BaseTy] -> [Set BaseTy]) -> [BaseTy] -> Set BaseTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BaseTy -> Set BaseTy) -> [BaseTy] -> [Set BaseTy]
forall a b. (a -> b) -> [a] -> [b]
map (\BaseTy
t -> [BaseTy] -> Set BaseTy
forall a. Ord a => [a] -> Set a
S.fromList (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] -> Set BaseTy) -> [BaseTy] -> Set BaseTy
forall a b. (a -> b) -> a -> b
$ [BaseTy]
ts
 where
  isects :: [Set BaseTy] -> Set BaseTy
isects = (Set BaseTy -> Set BaseTy -> Set BaseTy)
-> [Set BaseTy] -> Set BaseTy
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Set BaseTy -> Set BaseTy -> Set BaseTy
forall a. Ord a => Set a -> Set a -> Set a
S.intersection

ubsBySort, lbsBySort :: TyVarInfoMap -> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Set BaseTy
ubsBySort :: TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Set BaseTy
ubsBySort TyVarInfoMap
vm RelMap
rm = TyVarInfoMap
-> RelMap
-> Dir
-> [BaseTy]
-> Sort
-> Set (Name Type)
-> Set BaseTy
allBySort TyVarInfoMap
vm RelMap
rm Dir
SuperTy
lbsBySort :: TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Set BaseTy
lbsBySort TyVarInfoMap
vm RelMap
rm = TyVarInfoMap
-> RelMap
-> Dir
-> [BaseTy]
-> Sort
-> Set (Name Type)
-> Set BaseTy
allBySort 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 ann), State SolutionLimit] r =>
  TyVarInfoMap ->
  Graph UAtom ->
  Sem r [S]
solveGraph :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Fresh, Error SolveError, Output (Message ann),
    State SolutionLimit]
  r =>
TyVarInfoMap -> Graph UAtom -> Sem r [S]
solveGraph TyVarInfoMap
vm Graph UAtom
g = do
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Solving graph..."
  Graph UAtom -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty Graph UAtom
g
  (Substitution BaseTy -> S) -> [Substitution BaseTy] -> [S]
forall a b. (a -> b) -> [a] -> [b]
map (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 ann (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Output (Message ann), State SolutionLimit] 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 a b. (a -> b) -> Substitution a -> Substitution b
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
forall a b. Coercible a b => a -> b
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 b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
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 b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
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, Output (Message ann), State SolutionLimit] r =>
    RelMap ->
    Sem r [Substitution BaseTy]
  go :: forall ann (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Output (Message ann), State SolutionLimit] r =>
RelMap -> Sem r [Substitution BaseTy]
go relMap :: RelMap
relMap@(RelMap Map (Name Type, Dir) Rels
rm) = Sem r [Substitution BaseTy] -> Sem r [Substitution BaseTy]
forall (r :: [(* -> *) -> * -> *]) ann a.
(Member (State SolutionLimit) r, Member (Output (Message ann)) r,
 Monoid a) =>
Sem r a -> Sem r a
withSolutionLimit (Sem r [Substitution BaseTy] -> Sem r [Substitution BaseTy])
-> Sem r [Substitution BaseTy] -> Sem r [Substitution BaseTy]
forall a b. (a -> b) -> a -> b
$ do
    RelMap -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty RelMap
relMap
    case [Name Type]
as of
      -- No variables left that have base type constraints.
      [] -> do
        -- Found a solution, decrement the counter.
        Sem r ()
forall (r :: [(* -> *) -> * -> *]).
Member (State SolutionLimit) r =>
Sem r ()
countSolution
        [Substitution BaseTy] -> Sem r [Substitution BaseTy]
forall a. a -> Sem r a
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 ann) -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug (Sem r (Doc ann) -> Sem r ()) -> Sem r (Doc ann) -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Solving for" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Name Type -> Sem r (Doc ann)
forall t (r :: [(* -> *) -> * -> *]) ann.
Pretty t =>
t -> Sem r (Doc ann)
pretty' Name Type
a
        let ss :: [Substitution BaseTy]
ss = Name Type -> [Substitution BaseTy]
solveVar Name Type
a
        [Substitution BaseTy] -> Sem r ()
forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty [Substitution BaseTy]
ss

        -- 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.
        [[Substitution BaseTy]]
ss' <- [Substitution BaseTy]
-> (Substitution BaseTy -> Sem r [Substitution BaseTy])
-> Sem r [[Substitution BaseTy]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Substitution BaseTy]
ss ((Substitution BaseTy -> Sem r [Substitution BaseTy])
 -> Sem r [[Substitution BaseTy]])
-> (Substitution BaseTy -> Sem r [Substitution BaseTy])
-> Sem r [[Substitution BaseTy]]
forall a b. (a -> b) -> a -> b
$ \Substitution BaseTy
s ->
          (Substitution BaseTy -> Substitution BaseTy)
-> [Substitution BaseTy] -> [Substitution BaseTy]
forall a b. (a -> b) -> [a] -> [b]
map (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 ann (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Output (Message ann), State SolutionLimit] 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
forall a b. Coercible a b => a -> b
coerce Name Type
a) Substitution BaseTy
s) RelMap
relMap)
        [Substitution BaseTy] -> Sem r [Substitution BaseTy]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([[Substitution BaseTy]] -> [Substitution BaseTy]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join [[Substitution BaseTy]]
ss')
   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

    -- XXX the right way to do this is to keep track of the
    -- polarity of each variable.  For variables that have only
    -- one polarity we can pick the greatest or least solution as
    -- appropriate.  For other variables, we have to return all of
    -- them.

    -- Solve for a variable, returning all possible substitutions.
    solveVar :: Name Type -> [Substitution BaseTy]
    solveVar :: Name Type -> [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]
Traversal
  ((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.
        --
        -- If the sort is 'bool', we'll pick the Boolean base
        -- type, since there are no other sorts which could cause
        -- a conflict as in #192.
        --
        -- Otherwise, we 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.
        --
        -- Hmm, no, this is wrong!  E.g. we could have a QCmp
        -- constraint, in which case something like Char or Bool
        -- could be OK...  In any case, this is really just to be
        -- able to show users some sample types, it's not an issue
        -- of soundness.  We don't (can't?) guarantee to return ALL possible types.

        ([], []) ->
          -- Debug.trace (show v ++ " has no sub- or supertypes.")
          -- Pick some base type with an appropriate sort.
          (BaseTy -> Substitution BaseTy)
-> [BaseTy] -> [Substitution BaseTy]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Name BaseTy
forall a b. Coercible a b => a -> b
coerce Name Type
v Name BaseTy -> BaseTy -> Substitution BaseTy
forall a. Name a -> a -> Substitution a
|->) ([BaseTy] -> [Substitution BaseTy])
-> [BaseTy] -> [Substitution BaseTy]
forall a b. (a -> b) -> a -> b
$ (BaseTy -> Bool) -> [BaseTy] -> [BaseTy]
forall a. (a -> Bool) -> [a] -> [a]
filter (BaseTy -> Sort -> Bool
`hasSort` TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v) [BaseTy
N, BaseTy
Z, BaseTy
F, BaseTy
Q, BaseTy
B, BaseTy
C]
        -- Only supertypes.  Just assign a to their inf, if one exists.
        ([BaseTy]
bsupers, []) ->
          -- Debug.trace (show v ++ " has only supertypes (" ++ show bsupers ++ ")") $
          (BaseTy -> Substitution BaseTy)
-> [BaseTy] -> [Substitution BaseTy]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Name BaseTy
forall a b. Coercible a b => a -> b
coerce Name Type
v Name BaseTy -> BaseTy -> Substitution BaseTy
forall a. Name a -> a -> Substitution a
|->) ([BaseTy] -> [Substitution BaseTy])
-> (Set BaseTy -> [BaseTy]) -> Set BaseTy -> [Substitution BaseTy]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set BaseTy -> [BaseTy]
forall a. Set a -> [a]
S.toList (Set BaseTy -> [Substitution BaseTy])
-> Set BaseTy -> [Substitution BaseTy]
forall a b. (a -> b) -> a -> b
$
            TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Set BaseTy
lbsBySort
              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 ("varmap: " ++ 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)))) $
          (BaseTy -> Substitution BaseTy)
-> [BaseTy] -> [Substitution BaseTy]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Name BaseTy
forall a b. Coercible a b => a -> b
coerce Name Type
v Name BaseTy -> BaseTy -> Substitution BaseTy
forall a. Name a -> a -> Substitution a
|->) ([BaseTy] -> [Substitution BaseTy])
-> (Set BaseTy -> [BaseTy]) -> Set BaseTy -> [Substitution BaseTy]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set BaseTy -> [BaseTy]
forall a. Set a -> [a]
S.toList (Set BaseTy -> [Substitution BaseTy])
-> Set BaseTy -> [Substitution BaseTy]
forall a b. (a -> b) -> a -> b
$
            TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Set BaseTy
ubsBySort
              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.
        ([BaseTy]
bsupers, [BaseTy]
bsubs) ->
          let mub :: Maybe BaseTy
mub = 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)))
              mlb :: Maybe BaseTy
mlb = 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)))
           in case (Maybe BaseTy
mlb, Maybe BaseTy
mub) of
                (Just BaseTy
lb, Just BaseTy
ub) ->
                  (BaseTy -> Substitution BaseTy)
-> [BaseTy] -> [Substitution BaseTy]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Name BaseTy
forall a b. Coercible a b => a -> b
coerce Name Type
v Name BaseTy -> BaseTy -> Substitution BaseTy
forall a. Name a -> a -> Substitution a
|->) ((BaseTy -> Bool) -> [BaseTy] -> [BaseTy]
forall a. (a -> Bool) -> [a] -> [a]
filter (BaseTy -> BaseTy -> Bool
`isSubB` BaseTy
ub) (BaseTy -> [BaseTy]
supertypes BaseTy
lb))
                (Maybe BaseTy, Maybe BaseTy)
_ -> []