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

-----------------------------------------------------------------------------

-----------------------------------------------------------------------------

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

import Unbound.Generics.LocallyNameless (
  Alpha,
  Name,
  Subst,
  fv,
  name2Integer,
  string2Name,
  substs,
 )

import Data.Coerce
import GHC.Generics (Generic)

import Control.Arrow ((&&&), (***))
import Control.Lens hiding (use, (%=), (.=))
import Control.Monad (unless, zipWithM)
import Data.Bifunctor (first, second)
import Data.Either (partitionEithers)
import Data.List (
  find,
  foldl',
  intersect,
  partition,
 )
import Data.Map (Map, (!))
import qualified Data.Map as M
import Data.Maybe (
  fromJust,
  fromMaybe,
  mapMaybe,
 )
import Data.Monoid (First (..))
import Data.Set (Set)
import qualified Data.Set as S
import Data.Tuple

import Disco.Effects.Fresh
import Disco.Effects.State
import Polysemy
import Polysemy.Error
import Polysemy.Input
import Polysemy.Output

import Disco.Messages
import Disco.Pretty hiding ((<>))
import Disco.Subst
import qualified Disco.Subst as Subst
import Disco.Typecheck.Constraints
import Disco.Typecheck.Graph (Graph)
import qualified Disco.Typecheck.Graph as G
import Disco.Typecheck.Unify
import Disco.Types
import Disco.Types.Qualifiers
import Disco.Types.Rules

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

-- | Type of errors which can be generated by the constraint solving
--   process.
data SolveError where
  NoWeakUnifier :: SolveError
  NoUnify :: SolveError
  UnqualBase :: Qualifier -> BaseTy -> SolveError
  Unqual :: Qualifier -> Type -> SolveError
  QualSkolem :: Qualifier -> Name Type -> SolveError
  deriving (Int -> SolveError -> ShowS
[SolveError] -> ShowS
SolveError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SolveError] -> ShowS
$cshowList :: [SolveError] -> ShowS
show :: SolveError -> String
$cshow :: SolveError -> String
showsPrec :: Int -> SolveError -> ShowS
$cshowsPrec :: Int -> SolveError -> ShowS
Show)

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

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

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

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

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

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

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

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

--------------------------------------------------
-- 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TyVarInfo] -> ShowS
$cshowList :: [TyVarInfo] -> ShowS
show :: TyVarInfo -> String
$cshow :: TyVarInfo -> String
showsPrec :: Int -> TyVarInfo -> ShowS
$cshowsPrec :: Int -> TyVarInfo -> ShowS
Show)

makeLenses ''TyVarInfo

instance Pretty TyVarInfo where
  pretty :: forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
TyVarInfo -> Sem r (Doc ann)
pretty (TVI (First Maybe Ilk
ilk) Sort
s) = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc ann
"?") forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Maybe Ilk
ilk forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ann)
"%" forall a. Semigroup a => a -> a -> a
<> forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Sort
s

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

-- | 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 forall a. Semigroup a => a -> a -> a
<> First Ilk
i2) (Sort
s1 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TyVarInfoMap] -> ShowS
$cshowList :: [TyVarInfoMap] -> ShowS
show :: TyVarInfoMap -> String
$cshow :: TyVarInfoMap -> String
showsPrec :: Int -> TyVarInfoMap -> ShowS
$cshowsPrec :: Int -> TyVarInfoMap -> ShowS
Show)

instance Pretty TyVarInfoMap where
  pretty :: forall (r :: [(* -> *) -> * -> *]) ann.
Members '[Reader PA, LFresh] r =>
TyVarInfoMap -> Sem r (Doc ann)
pretty (VM Map (Name Type) TyVarInfo
m) = forall t (r :: [(* -> *) -> * -> *]) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Map (Name Type) TyVarInfo
m

-- | 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 = forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name Type
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM

-- | 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a b. (a -> b) -> a -> b
$ \Map (Name Type) TyVarInfo
vm -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip (\Name Type
v -> forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name Type
v (Ilk -> Sort -> TyVarInfo
mkTVI Ilk
Skolem forall a. Monoid a => a
mempty))) Map (Name Type) TyVarInfo
vm [Name Type]
vs

-- | 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 (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. Semigroup a => a -> a -> a
(<>) Map (Name Type) TyVarInfo
sm1 Map (Name Type) TyVarInfo
sm2)

instance Monoid TyVarInfoMap where
  mempty :: TyVarInfoMap
mempty = Map (Name Type) TyVarInfo -> TyVarInfoMap
VM forall k a. Map k a
M.empty
  mappend :: TyVarInfoMap -> TyVarInfoMap -> TyVarInfoMap
mappend = forall a. Semigroup a => a -> a -> a
(<>)

-- | 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 = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sort
topSort (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Lens' TyVarInfo Sort
tyVarSort) (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name Type
v Map (Name Type) TyVarInfo
m)

-- | 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 forall s a. s -> Getting (First a) s a -> Maybe a
^? forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Name Type
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TyVarInfo (First Ilk)
tyVarIlk) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. First a -> Maybe a
getFirst

-- | 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 (forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Name Type
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Prism (Maybe a) (Maybe b) a b
_Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TyVarInfo Sort
tyVarSort forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall a. Ord a => Set a -> Set a -> Set a
`S.union` Sort
s))

---------------------------------
-- 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 = forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
error String
errMsg) (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup k
k Map k a
m)
 where
  errMsg :: String
errMsg =
    [String] -> String
unlines
      [ String
"Key lookup error:"
      , String
"  Key = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show k
k
      , String
"  Map = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Map k a
m
      , String
"  Location: " forall a. [a] -> [a] -> [a]
++ String
messg
      ]

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

solveConstraint ::
  Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx] r =>
  Constraint ->
  Sem r S
solveConstraint :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx]
  r =>
Constraint -> Sem r S
solveConstraint Constraint
c = do
  -- 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.

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

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

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

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

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

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

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

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

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

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

  forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty TyVarInfoMap
vm
  forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t (r :: [(* -> *) -> * -> *]) ann.
Pretty t =>
t -> Sem r (Doc ann)
pretty' forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Atom
x, Atom
y) -> Atom -> Type
TyAtom Atom
x Type -> Type -> SimpleConstraint
:<: Atom -> Type
TyAtom Atom
y)) [(Atom, Atom)]
atoms
  forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty S
theta_simp

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

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

  -- 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 = forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ((Name Type, First Ilk) -> Atom
mkAVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Lens' TyVarInfo (First Ilk)
tyVarIlk)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
M.assocs forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM forall a b. (a -> b) -> a -> b
$ TyVarInfoMap
vm
      g :: Graph Atom
g = forall a. (Show a, Ord a) => Set a -> [(a, a)] -> Graph a
mkConstraintGraph Set Atom
vars [(Atom, Atom)]
atoms

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

  -- 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.

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

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

  -- 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.

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

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

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

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

  -- ... 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.

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

  let vm' :: TyVarInfoMap
vm' = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name Type, Type) -> TyVarInfoMap -> TyVarInfoMap
updateVarMap TyVarInfoMap
vm (forall a. Substitution a -> [(Name a, a)]
Subst.toList S
theta_cyc)
       where
        updateVarMap :: (Name Type, Type) -> TyVarInfoMap -> TyVarInfoMap
        updateVarMap :: (Name Type, Type) -> TyVarInfoMap -> TyVarInfoMap
updateVarMap (Name Type
x, TyAtom (AVar (U Name Type
y))) TyVarInfoMap
vmm = Name Type -> Sort -> TyVarInfoMap -> TyVarInfoMap
extendSort Name Type
y (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vmm Name Type
x) TyVarInfoMap
vmm
        updateVarMap (Name Type, Type)
_ TyVarInfoMap
vmm = TyVarInfoMap
vmm

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

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

  -- 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''' <- 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.

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

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

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

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

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

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

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

decomposeQual ::
  Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
  Type ->
  Qualifier ->
  Sem r TyVarInfoMap
decomposeQual :: forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Type -> Qualifier -> Sem r TyVarInfoMap
decomposeQual = forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go forall a. Set a
S.empty
 where
  go ::
    Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
    Set (String, [Type], Qualifier) ->
    Type ->
    Qualifier ->
    Sem r TyVarInfoMap

  -- 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 = 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) forall a. Ord a => a -> Set a -> Bool
`S.member` Set (String, [Type], Qualifier)
seen of
      Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
      Bool
False -> do
        TyDefCtx
tyDefns <- forall i (r :: [(* -> *) -> * -> *]). Member (Input i) r => Sem r i
input @TyDefCtx
        case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
t TyDefCtx
tyDefns of
          Maybe TyDefBody
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show String
t forall a. [a] -> [a] -> [a]
++ String
" not in ty defn map!!"
          Just (TyDefBody [String]
_ [Type] -> Type
body) -> do
            let ty' :: Type
ty' = [Type] -> Type
body [Type]
tys
            forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go (forall a. Ord a => a -> Set a -> Set a
S.insert (String
t, [Type]
tys, Qualifier
q) Set (String, [Type], Qualifier)
seen) Type
ty' Qualifier
q

  -- 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 = 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 -> forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> SolveError
Unqual Qualifier
q Type
ty
    Just [Maybe Qualifier]
qs -> forall a. Monoid a => [a] -> a
mconcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
Set (String, [Type], Qualifier)
-> Type -> Qualifier -> Sem r TyVarInfoMap
go Set (String, [Type], Qualifier)
seen) [Type]
tys [Maybe Qualifier]
qs

checkQual ::
  Members '[Fresh, Error SolveError] r =>
  Qualifier ->
  Atom ->
  Sem r TyVarInfoMap
checkQual :: forall (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError] r =>
Qualifier -> Atom -> Sem r TyVarInfoMap
checkQual Qualifier
q (AVar (U Name Type
v)) = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Name Type) TyVarInfo -> TyVarInfoMap
VM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. k -> a -> Map k a
M.singleton Name Type
v forall a b. (a -> b) -> a -> b
$ Ilk -> Sort -> TyVarInfo
mkTVI Ilk
Unification (forall a. a -> Set a
S.singleton Qualifier
q)
checkQual Qualifier
q (AVar (S Name Type
v)) = forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ Qualifier -> Name Type -> SolveError
QualSkolem Qualifier
q Name Type
v
checkQual Qualifier
q (ABase BaseTy
bty) =
  case BaseTy -> Qualifier -> Bool
hasQual BaseTy
bty Qualifier
q of
    Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
    Bool
False -> forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ Qualifier -> BaseTy -> SolveError
UnqualBase Qualifier
q BaseTy
bty

--------------------------------------------------
-- 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', 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."
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]) a.
Integer -> Sem (Fresh : r) a -> Sem r a
runFresh' Integer
n (forall s (r :: [(* -> *) -> * -> *]) a.
s -> Sem (State s : r) a -> Sem r s
execState (TyVarInfoMap
-> [SimpleConstraint] -> S -> Set SimpleConstraint -> SimplifyState
SS TyVarInfoMap
origVM [SimpleConstraint]
cs forall a. Substitution a
idS forall a. Set a
S.empty) forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError,
    Output (Message ann), Input TyDefCtx]
  r =>
Sem r ()
simplify')
 where
  fvNums :: Alpha a => [a] -> [Integer]
  fvNums :: forall a. Alpha a => [a] -> [Integer]
fvNums = forall a b. (a -> b) -> [a] -> [b]
map (forall a. Name a -> Integer
name2Integer :: Name Type -> Integer) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf forall a (f :: * -> *) b.
(Alpha a, Typeable b, Contravariant f, Applicative f) =>
(Name b -> f (Name b)) -> a -> f a
fv

  -- 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 = forall {a}. (Num a, Ord a) => [a] -> a
maximum0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Alpha a => [a] -> [Integer]
fvNums forall a b. (a -> b) -> a -> b
$ [SimpleConstraint]
cs
  n :: Integer
n = forall a. Enum a => a -> a
succ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer
n1 forall a. a -> [a] -> [a]
:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Alpha a => [a] -> [Integer]
fvNums forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [k]
M.keys forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Map (Name Type) TyVarInfo
unVM forall a b. (a -> b) -> a -> b
$ TyVarInfoMap
origVM

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

  -- 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 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible: simplify left non-atomic or non-subtype constraint " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SimpleConstraint
c

  -- 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 <- forall (r :: [(* -> *) -> * -> *]).
Members '[State SimplifyState, Fresh, Error SolveError] r =>
Sem r (Maybe SimpleConstraint)
pickSimplifiable
    case Maybe SimpleConstraint
mc of
      Maybe SimpleConstraint
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Just SimpleConstraint
s -> do
        forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Simplifying:" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: [(* -> *) -> * -> *]) ann.
Pretty t =>
t -> Sem r (Doc ann)
pretty' SimpleConstraint
s

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

  -- 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 <- forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' SimplifyState [SimpleConstraint]
ssConstraints
    case forall a. (a -> Bool) -> [a] -> Maybe (a, [a])
pick SimpleConstraint -> Bool
simplifiable [SimpleConstraint]
curCs of
      Maybe (SimpleConstraint, [SimpleConstraint])
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      Just (SimpleConstraint
a, [SimpleConstraint]
as) -> do
        Lens' SimplifyState [SimpleConstraint]
ssConstraints forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> a -> Sem r ()
.= [SimpleConstraint]
as
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just SimpleConstraint
a)

  -- Pick 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
_ [] = forall a. Maybe a
Nothing
  pick a -> Bool
p (a
a : [a]
as)
    | a -> Bool
p a
a = forall a. a -> Maybe a
Just (a
a, [a]
as)
    | Bool
otherwise = forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (a
a forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> Maybe (a, [a])
pick a -> Bool
p [a]
as

  -- 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 <- forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' SimplifyState (Set SimpleConstraint)
ssSeen
    case SimpleConstraint
c forall a. Ord a => a -> Set a -> Bool
`S.member` Set SimpleConstraint
seen of
      Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Bool
False -> do
        Lens' SimplifyState (Set SimpleConstraint)
ssSeen forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= forall a. Ord a => a -> Set a -> Set a
S.insert SimpleConstraint
c
        forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
  r =>
SimpleConstraint -> Sem r ()
simplifyOne' SimpleConstraint
c

  simplifyOne' ::
    Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r =>
    SimpleConstraint ->
    Sem r ()

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

  -- 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 {}) =
    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 forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
t TyDefCtx
tyDefns of
      Maybe TyDefBody
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show String
t forall a. [a] -> [a] -> [a]
++ String
" not in ty defn map!"
      Just (TyDefBody [String]
_ [Type] -> Type
body) ->
        Lens' SimplifyState [SimpleConstraint]
ssConstraints forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= (([Type] -> Type
body [Type]
ts Type -> Type -> SimpleConstraint
:<: Type
ty2) forall a. a -> [a] -> [a]
:)

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

  -- Given a subtyping constraint between two type constructors,
  -- decompose it if the constructors are the same (or fail if they
  -- aren't), taking into account the variance of each argument to
  -- the constructor.  Container types are a special case;
  -- recursively generate a subtyping constraint for their
  -- constructors as well.
  simplifyOne' (TyCon c1 :: Con
c1@(CContainer Atom
ctr1) [Type]
tys1 :<: TyCon (CContainer Atom
ctr2) [Type]
tys2) =
    Lens' SimplifyState [SimpleConstraint]
ssConstraints
      forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= ( ( (Atom -> Type
TyAtom Atom
ctr1 Type -> Type -> SimpleConstraint
:<: Atom -> Type
TyAtom Atom
ctr2)
              forall a. a -> [a] -> [a]
: forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Variance -> Type -> Type -> SimpleConstraint
variance (Con -> [Variance]
arity Con
c1) [Type]
tys1 [Type]
tys2
           )
            forall a. [a] -> [a] -> [a]
++
         )
  simplifyOne' (TyCon Con
c1 [Type]
tys1 :<: TyCon Con
c2 [Type]
tys2)
    | Con
c1 forall a. Eq a => a -> a -> Bool
/= Con
c2 = forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
    | Bool
otherwise =
        Lens' SimplifyState [SimpleConstraint]
ssConstraints forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= (forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Variance -> Type -> Type -> SimpleConstraint
variance (Con -> [Variance]
arity Con
c1) [Type]
tys1 [Type]
tys2 forall a. [a] -> [a] -> [a]
++)
  -- 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]
_) = forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
  r =>
Name Type -> Con -> SimpleConstraint -> Sem r ()
expandStruct Name Type
a Con
c SimpleConstraint
con
  simplifyOne' con :: SimpleConstraint
con@(TyCon Con
c [Type]
_ :<: TyVar Name Type
a) = forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
  r =>
Name Type -> Con -> SimpleConstraint -> Sem r ()
expandStruct Name Type
a Con
c SimpleConstraint
con
  -- 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Bool
False -> forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
  simplifyOne' (Type
s :<: Type
t) =
    forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! simplifyOne' " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
s forall a. [a] -> [a] -> [a]
++ String
" :<: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
t

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

  -- 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
    Lens' SimplifyState S
ssSubst forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= (S
s' forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@)
    Lens' SimplifyState [SimpleConstraint]
ssConstraints forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Lens' s a -> (a -> a) -> Sem r ()
%= forall b a. Subst b a => Substitution b -> a -> a
applySubst S
s'
    forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
  r =>
S -> Sem r ()
substVarMap S
s'

  substVarMap ::
    Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r =>
    S ->
    Sem r ()
  substVarMap :: forall (r :: [(* -> *) -> * -> *]).
Members
  '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx]
  r =>
S -> Sem r ()
substVarMap S
s' = do
    TyVarInfoMap
vm <- forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' SimplifyState TyVarInfoMap
ssVarMap

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

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

    -- 2. Decompose the resulting qualifier constraints

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

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

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

  -- 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 = forall a. (Show a, Ord a) => Set a -> Set (a, a) -> Graph a
G.mkGraph Set a
nodes (forall a. Ord a => [a] -> Set a
S.fromList [(a, a)]
cs)
 where
  nodes :: Set a
nodes = Set a
as forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. Ord a => [a] -> Set a
S.fromList ([(a, a)]
cs forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s t a b. Each s t a b => Traversal s t a b
each)

--------------------------------------------------
-- 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 = forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Atom -> Bool
isSkolem) forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Graph a -> [Set a]
G.wcc Graph Atom
graph

      ok :: Set Atom -> Bool
ok Set Atom
wcc =
        forall a. Set a -> Int
S.size (forall a. (a -> Bool) -> Set a -> Set a
S.filter Atom -> Bool
isSkolem Set Atom
wcc) forall a. Ord a => a -> a -> Bool
<= Int
1
          Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
            ( \case
                ABase BaseTy
_ -> Bool
False
                AVar (S Name Type
_) -> Bool
True
                AVar (U Name Type
v) -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (forall a. Set a -> Bool
S.null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Lens' TyVarInfo Sort
tyVarSort) (Name Type -> TyVarInfoMap -> Maybe TyVarInfo
lookupVM Name Type
v TyVarInfoMap
vm)
            )
            Set Atom
wcc

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

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

  -- take all good sets and
  --   (1) delete them from the graph
  --   (2) unify them all with the skolem
  forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
graph forall a. Substitution a
idS [Set Atom]
good
 where
  noSkolems :: Atom -> UAtom
  noSkolems :: Atom -> UAtom
noSkolems (ABase BaseTy
b) = BaseTy -> UAtom
UB BaseTy
b
  noSkolems (AVar (U Name Type
v)) = Name Type -> UAtom
UV Name Type
v
  noSkolems (AVar (S Name Type
v)) = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Skolem " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name Type
v forall a. [a] -> [a] -> [a]
++ String
" remaining in noSkolems"

  unifyWCCs ::
    Members '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
    Graph Atom ->
    S ->
    [Set Atom] ->
    Sem r (Graph UAtom, S)
  unifyWCCs :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
g S
s [] = forall (m :: * -> *) a. Monad m => a -> m a
return (forall b a. Ord b => (a -> b) -> Graph a -> Graph b
G.map Atom -> UAtom
noSkolems Graph Atom
g, S
s)
  unifyWCCs Graph Atom
g S
s (Set Atom
u : [Set Atom]
us) = do
    forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Unifying" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: [(* -> *) -> * -> *]) ann.
Pretty t =>
t -> Sem r (Doc ann)
pretty' (Set Atom
u forall a. a -> [a] -> [a]
: [Set Atom]
us) forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ann)
"..."

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

    let g' :: Graph Atom
g' = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. (Show a, Ord a) => a -> Graph a -> Graph a
G.delete) Graph Atom
g Set Atom
u

        ms' :: Maybe (Substitution Atom)
ms' = TyDefCtx -> [Atom] -> Maybe (Substitution Atom)
unifyAtoms TyDefCtx
tyDefns (forall a. Set a -> [a]
S.toList Set Atom
u)
    case Maybe (Substitution Atom)
ms' of
      Maybe (Substitution Atom)
Nothing -> forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify
      Just Substitution Atom
s' -> forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)
unifyWCCs Graph Atom
g' (Substitution Atom -> S
atomToTypeSubst Substitution Atom
s' forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ S
s) [Set Atom]
us

--------------------------------------------------
-- 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 = forall a b (r :: [(* -> *) -> * -> *]).
(Subst a a, Ord a, Members '[Error SolveError] r) =>
(Substitution a -> Substitution b)
-> ([a] -> Maybe (Substitution a))
-> Graph a
-> Sem r (Graph a, Substitution b)
elimCyclesGen Substitution UAtom -> S
uatomToTypeSubst (TyDefCtx -> [UAtom] -> Maybe (Substitution UAtom)
unifyUAtoms TyDefCtx
tyDefns)

elimCyclesGen ::
  forall a b r.
  (Subst a a, Ord a, Members '[Error SolveError] r) =>
  (Substitution a -> Substitution b) ->
  ([a] -> Maybe (Substitution a)) ->
  Graph a ->
  Sem r (Graph a, Substitution b)
elimCyclesGen :: forall a b (r :: [(* -> *) -> * -> *]).
(Subst a a, Ord a, Members '[Error SolveError] r) =>
(Substitution a -> Substitution b)
-> ([a] -> Maybe (Substitution a))
-> Graph a
-> Sem r (Graph a, Substitution b)
elimCyclesGen Substitution a -> Substitution b
genSubst [a] -> Maybe (Substitution a)
genUnify Graph a
g =
  forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Maybe a -> Sem r a
note SolveError
NoUnify forall a b. (a -> b) -> a -> b
$
    (forall b a. Ord b => (a -> b) -> Graph a -> Graph b
G.map forall a b. (a, b) -> a
fst forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (Substitution a -> Substitution b
genSubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (t :: * -> *).
(Subst a a, Foldable t) =>
t (Substitution a) -> Substitution a
compose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Graph a -> Set a
G.nodes)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Graph (a, Substitution a))
g'
 where
  g' :: Maybe (Graph (a, Substitution a))
  g' :: Maybe (Graph (a, Substitution a))
g' = forall a. Ord a => Graph (Maybe a) -> Maybe (Graph a)
G.sequenceGraph forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> Graph a -> Graph b
G.map Set a -> Maybe (a, Substitution a)
unifySCC (forall a. Ord a => Graph a -> Graph (Set a)
G.condensation Graph a
g)

  unifySCC :: Set a -> Maybe (a, Substitution a)
  unifySCC :: Set a -> Maybe (a, Substitution a)
unifySCC Set a
uatoms = case forall a. Set a -> [a]
S.toList Set a
uatoms of
    [] -> forall a. HasCallStack => String -> a
error String
"Impossible! unifySCC on the empty set"
    as :: [a]
as@(a
a : [a]
_) -> (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall b a. Subst b a => Substitution b -> a -> a
applySubst a
a forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall a. a -> a
id) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Maybe (Substitution a)
genUnify [a]
as

------------------------------------------------------------
-- 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) = forall a b. a -> Either a b
Left (BaseTy
b1, BaseTy
b2)
isBaseEdge (UAtom, UAtom)
e = forall a b. b -> Either a b
Right (UAtom, UAtom)
e

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

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

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

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

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

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

-- | 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
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Map k a
M.delete (Name Type
x, Dir
SuperTy)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Map k a
M.delete (Name Type
x, Dir
SubTy)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b k. (a -> b) -> Map k a -> Map k b
M.map (\r :: Rels
r@(Rels Set BaseTy
b Set (Name Type)
v) -> if Name Type
x forall a. Ord a => a -> Set a -> Bool
`S.member` Set (Name Type)
v then Set BaseTy -> Set (Name Type) -> Rels
Rels (forall a. Ord a => a -> Set a -> Set a
S.insert BaseTy
ty Set BaseTy
b) (forall a. Ord a => a -> Set a -> Set a
S.delete Name Type
x Set (Name Type)
v) else Rels
r)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelMap -> Map (Name Type, Dir) Rels
unRelMap

-- | 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
  forall {a}. [a] -> (a -> Bool) -> [a]
keep (Dir -> BaseTy -> [BaseTy]
dirtypes Dir
dir BaseTy
t) 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,
      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,
            forall (t :: * -> *) a. Foldable t => t a -> (a -> Bool) -> Bool
exists (Dir -> BaseTy -> [BaseTy]
dirtypes (Dir -> Dir
other Dir
dir) BaseTy
t') forall a b. (a -> b) -> a -> b
$ \BaseTy
t'' ->
              -- 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.
                forall (t :: * -> *) a. Foldable t => t a -> (a -> Bool) -> Bool
forAll
                  (Rels -> Set BaseTy
baseRels (forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"dirtypesBySort, beta rel" Map (Name Type, Dir) Rels
relMap (Name Type
beta, Dir -> Dir
other Dir
dir)))
                  (Dir -> BaseTy -> BaseTy -> Bool
isDirB Dir
dir BaseTy
t'')
        )
 where
  -- 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
  exists :: forall (t :: * -> *) a. Foldable t => t a -> (a -> Bool) -> Bool
exists = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any
  keep :: [a] -> (a -> Bool) -> [a]
keep = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. (a -> Bool) -> [a] -> [a]
filter

-- | 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 -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\BaseTy
lim -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\BaseTy
u -> Dir -> BaseTy -> BaseTy -> Bool
isDirB Dir
dir BaseTy
u BaseTy
lim) [BaseTy]
is) [BaseTy]
is)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[BaseTy]] -> [BaseTy]
isects
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\BaseTy
t -> TyVarInfoMap
-> RelMap -> Dir -> BaseTy -> Sort -> Set (Name Type) -> [BaseTy]
dirtypesBySort TyVarInfoMap
vm RelMap
rm Dir
dir BaseTy
t Sort
s Set (Name Type)
x)
    forall a b. (a -> b) -> a -> b
$ [BaseTy]
ts
 where
  isects :: [[BaseTy]] -> [BaseTy]
isects = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 forall a. Eq a => [a] -> [a] -> [a]
intersect

lubBySort, glbBySort :: TyVarInfoMap -> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort :: TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort TyVarInfoMap
vm RelMap
rm = TyVarInfoMap
-> RelMap
-> Dir
-> [BaseTy]
-> Sort
-> Set (Name Type)
-> Maybe BaseTy
limBySort TyVarInfoMap
vm RelMap
rm Dir
SuperTy
glbBySort :: TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
glbBySort TyVarInfoMap
vm RelMap
rm = TyVarInfoMap
-> RelMap
-> Dir
-> [BaseTy]
-> Sort
-> Set (Name Type)
-> Maybe BaseTy
limBySort TyVarInfoMap
vm RelMap
rm Dir
SubTy

-- | 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)] r =>
  TyVarInfoMap ->
  Graph UAtom ->
  Sem r S
solveGraph :: forall ann (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output (Message ann)] r =>
TyVarInfoMap -> Graph UAtom -> Sem r S
solveGraph TyVarInfoMap
vm Graph UAtom
g = Substitution Atom -> S
atomToTypeSubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution BaseTy -> Substitution Atom
unifyWCC forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ann (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output (Message ann)] r =>
RelMap -> Sem r (Substitution BaseTy)
go RelMap
topRelMap
 where
  unifyWCC :: Substitution BaseTy -> Substitution Atom
  unifyWCC :: Substitution BaseTy -> Substitution Atom
unifyWCC Substitution BaseTy
s = forall a (t :: * -> *).
(Subst a a, Foldable t) =>
t (Substitution a) -> Substitution a
compose (forall a b. (a -> b) -> [a] -> [b]
map Set (Name Type) -> Substitution Atom
mkEquateSubst [Set (Name Type)]
wccVarGroups) forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BaseTy -> Atom
ABase Substitution BaseTy
s
   where
    wccVarGroups :: [Set (Name Type)]
    wccVarGroups :: [Set (Name Type)]
wccVarGroups = forall a b. (a -> b) -> [a] -> [b]
map (forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map UAtom -> Name Type
getVar) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all UAtom -> Bool
uisVar) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Subst b a => Substitution b -> a -> a
applySubst Substitution BaseTy
s forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Graph a -> [Set a]
G.wcc Graph UAtom
g
    getVar :: UAtom -> Name Type
getVar (UV Name Type
v) = Name Type
v
    getVar (UB BaseTy
b) =
      forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
        String
"Impossible! Base type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BaseTy
b forall a. [a] -> [a] -> [a]
++ String
" in solveGraph.getVar"

    mkEquateSubst :: Set (Name Type) -> Substitution Atom
    mkEquateSubst :: Set (Name Type) -> Substitution Atom
mkEquateSubst = [Name Type] -> Substitution Atom
mkEquations forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
S.toList

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

  -- 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
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b k. (a -> b) -> Map k a -> Map k b
M.map
        ( forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Set BaseTy -> Set (Name Type) -> Rels
Rels
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Eq a => [a] -> Set a
S.fromAscList forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. Eq a => [a] -> Set a
S.fromAscList)
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [Either a b] -> ([a], [b])
partitionEithers
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map UAtom -> Either BaseTy (Name Type)
uatomToEither
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
S.toList
        )
      forall a b. (a -> b) -> a -> b
$ forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys (,Dir
SuperTy) Map (Name Type) (Set UAtom)
subMap forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys (,Dir
SubTy) Map (Name Type) (Set UAtom)
superMap

  subMap, superMap :: Map (Name Type) (Set UAtom)
  (Map (Name Type) (Set UAtom)
subMap, Map (Name Type) (Set UAtom)
superMap) = (Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom)
onlyVars forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom)
onlyVars) forall a b. (a -> b) -> a -> b
$ forall a.
(Show a, Ord a) =>
Graph a -> (Map a (Set a), Map a (Set a))
G.cessors Graph UAtom
g

  onlyVars :: Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom)
  onlyVars :: Map UAtom (Set UAtom) -> Map (Name Type) (Set UAtom)
onlyVars = forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys UAtom -> Name Type
fromVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey (\UAtom
a Set UAtom
_ -> UAtom -> Bool
uisVar UAtom
a)
   where
    fromVar :: UAtom -> Name Type
fromVar (UV Name Type
x) = Name Type
x
    fromVar UAtom
_ = forall a. HasCallStack => String -> a
error String
"Impossible! UB but uisVar."

  go ::
    Members '[Fresh, Error SolveError, Output (Message ann)] r =>
    RelMap ->
    Sem r (Substitution BaseTy)
  go :: forall ann (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output (Message ann)] r =>
RelMap -> Sem r (Substitution BaseTy)
go relMap :: RelMap
relMap@(RelMap Map (Name Type, Dir) Rels
rm) =
    forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty RelMap
relMap forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> case [Name Type]
as of
      -- No variables left that have base type constraints.
      [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Substitution a
idS
      -- Solve one variable at a time.  See below.
      (Name Type
a : [Name Type]
_) -> do
        forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Solving for" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: [(* -> *) -> * -> *]) ann.
Pretty t =>
t -> Sem r (Doc ann)
pretty' Name Type
a
        case Name Type -> Maybe (Substitution BaseTy)
solveVar Name Type
a of
          Maybe (Substitution BaseTy)
Nothing -> do
            forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Couldn't solve for" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: [(* -> *) -> * -> *]) ann.
Pretty t =>
t -> Sem r (Doc ann)
pretty' Name Type
a
            forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw SolveError
NoUnify

          -- If we solved for a, delete it from the maps, apply the
          -- resulting substitution to the remainder (updating the
          -- relMap appropriately), and recurse.  The substitution we
          -- want will be the composition of the substitution for a
          -- with the substitution generated by the recursive call.
          --
          -- Note we don't need to delete a from the TyVarInfoMap; we
          -- never use the set of keys from the TyVarInfoMap for
          -- anything (indeed, some variables might not be keys if
          -- they have an empty sort), so it doesn't matter if old
          -- variables hang around in it.
          Just Substitution BaseTy
s -> do
            forall ann (r :: [(* -> *) -> * -> *]) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty Substitution BaseTy
s
            (forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ Substitution BaseTy
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ann (r :: [(* -> *) -> * -> *]).
Members '[Fresh, Error SolveError, Output (Message ann)] r =>
RelMap -> Sem r (Substitution BaseTy)
go (Name Type -> BaseTy -> RelMap -> RelMap
substRel Name Type
a (forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall a. Name a -> Substitution a -> Maybe a
Subst.lookup (coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
a) Substitution BaseTy
s) RelMap
relMap)
   where
    -- 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 =
      forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> Bool
S.null forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rels -> Set BaseTy
baseRels forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveGraph.go.as" Map (Name Type, Dir) Rels
rm)
        forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys Map (Name Type, Dir) Rels
rm
    as :: [Name Type]
as = case [Name Type]
asBase of
      [] -> forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
/= Sort
topSort) forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys Map (Name Type, Dir) Rels
rm
      [Name Type]
_ -> [Name Type]
asBase

    -- Solve for a variable, failing if it has no solution, otherwise returning
    -- a substitution for it.
    solveVar :: Name Type -> Maybe (Substitution BaseTy)
    solveVar :: Name Type -> Maybe (Substitution BaseTy)
solveVar Name Type
v =
      case ((Name Type
v, Dir
SuperTy), (Name Type
v, Dir
SubTy)) forall a b. a -> (a -> b) -> b
& forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over forall (r :: * -> * -> *) a b.
Bitraversable r =>
Traversal (r a a) (r b b) a b
both (forall a. Set a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rels -> Set BaseTy
baseRels forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveGraph.solveVar" Map (Name Type, Dir) Rels
rm) of
        -- 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.

        ([], []) ->
          if TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
S.fromList [Qualifier
QBool]
            then forall a. a -> Maybe a
Just (coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
v forall a. Name a -> a -> Substitution a
|-> BaseTy
B)
            else -- Debug.trace (show v ++ " has no sub- or supertypes.  Assuming N as a subtype.")

              (coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
v forall a. Name a -> a -> Substitution a
|->)
                forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort
                  TyVarInfoMap
vm
                  RelMap
relMap
                  [BaseTy
N]
                  (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
                  (Rels -> Set (Name Type)
varRels (forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveVar none, rels" Map (Name Type, Dir) Rels
rm (Name Type
v, Dir
SubTy)))
        -- Only supertypes.  Just assign a to their inf, if one exists.
        ([BaseTy]
bsupers, []) ->
          -- Debug.trace (show v ++ " has only supertypes (" ++ show bsupers ++ ")") $
          (coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
v forall a. Name a -> a -> Substitution a
|->)
            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
glbBySort
              TyVarInfoMap
vm
              RelMap
relMap
              [BaseTy]
bsupers
              (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
              (Rels -> Set (Name Type)
varRels (forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveVar bsupers, rels" Map (Name Type, Dir) Rels
rm (Name Type
v, Dir
SuperTy)))
        -- Only subtypes.  Just assign a to their sup.
        ([], [BaseTy]
bsubs) ->
          -- Debug.trace (show v ++ " has only subtypes (" ++ show bsubs ++ ")") $
          -- Debug.trace ("sortmap: " ++ show vm) $
          -- Debug.trace ("relmap: " ++ show relMap) $
          -- Debug.trace ("sort for " ++ show v ++ ": " ++ show (getSort vm v)) $
          -- Debug.trace ("relvars: " ++ show (varRels (relMap ! (v,SubTy)))) $
          (coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
v forall a. Name a -> a -> Substitution a
|->)
            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort
              TyVarInfoMap
vm
              RelMap
relMap
              [BaseTy]
bsubs
              (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
              (Rels -> Set (Name Type)
varRels (forall k a.
(Ord k, Show k, Show (Map k a)) =>
String -> Map k a -> k -> a
lkup String
"solveVar bsubs, rels" Map (Name Type, Dir) Rels
rm (Name Type
v, Dir
SubTy)))
        -- Both successors and predecessors.  Both must have a
        -- valid bound, and the bounds must not overlap.  Assign a
        -- to the sup of its predecessors.
        ([BaseTy]
bsupers, [BaseTy]
bsubs) -> do
          BaseTy
ub <-
            TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
glbBySort
              TyVarInfoMap
vm
              RelMap
relMap
              [BaseTy]
bsupers
              (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
              (Rels -> Set (Name Type)
varRels (Map (Name Type, Dir) Rels
rm forall k a. Ord k => Map k a -> k -> a
! (Name Type
v, Dir
SuperTy)))
          BaseTy
lb <-
            TyVarInfoMap
-> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Maybe BaseTy
lubBySort
              TyVarInfoMap
vm
              RelMap
relMap
              [BaseTy]
bsubs
              (TyVarInfoMap -> Name Type -> Sort
getSort TyVarInfoMap
vm Name Type
v)
              (Rels -> Set (Name Type)
varRels (Map (Name Type, Dir) Rels
rm forall k a. Ord k => Map k a -> k -> a
! (Name Type
v, Dir
SubTy)))
          case BaseTy -> BaseTy -> Bool
isSubB BaseTy
lb BaseTy
ub of
            Bool
True -> forall a. a -> Maybe a
Just (coerce :: forall a b. Coercible a b => a -> b
coerce Name Type
v forall a. Name a -> a -> Substitution a
|-> BaseTy
lb)
            Bool
False -> forall a. Maybe a
Nothing