alms-0.6.0: src/Statics/Constraint.hs
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
module Statics.Constraint (
-- * The constraint solver interface
MonadConstraint(..), generalize, generalizeList, generalizeEx,
-- * An implementation of the interface
ConstraintT,
runConstraintT, mapConstraintT,
ConstraintState, constraintState0, pprConstraintState,
runConstraintIO,
) where
import Util
import Util.Trace
import Util.MonadRef
import qualified Syntax.Ppr as Ppr
import qualified Alt.Graph as Gr
import qualified Data.UnionFind as UF
import Type
import Statics.Error
import Prelude ()
import qualified Data.List as List
import qualified Data.Set as S
import qualified Data.Map as M
import qualified Data.Boolean.SatSolver as SAT
import Data.IORef (IORef)
---
--- A CONSTRAINT-SOLVING MONAD
---
class MonadSubst tv r m ⇒ MonadConstraint tv r m | m → tv r where
-- | Subtype and equality constraints
(<:), (=:) ∷ Type tv → Type tv → m ()
-- | Subqualifier constraint
(⊏:), (~:) ∷ (Qualifier q1 tv, Qualifier q2 tv) ⇒ q1 → q2 → m ()
-- | Constrain by the given variance
relate ∷ Variance → Type tv → Type tv → m ()
--
τ1 =: τ2 = τ1 <: τ2 >> τ2 <: τ1
τ1 ~: τ2 = τ1 ⊏: τ2 >> τ2 ⊏: τ1
relate variance τ1 τ2 = case variance of
Covariant → τ1 <: τ2
Contravariant → τ2 <: τ1
Invariant → τ1 =: τ2
QCovariant → τ1 ⊏: τ2
QContravariant → τ2 ⊏: τ1
QInvariant → τ1 ~: τ2
Omnivariant → return ()
--
-- | Get the set of pinned type variables.
getPinnedTVs ∷ m (S.Set tv)
-- | Run a computation in the context of some "pinned down" type
-- variables, which means that they won't be considered for
-- elimination or generalization.
withPinnedTVs ∷ Ftv a tv ⇒ a → m b → m b
-- | Update the list of pinned type variables to reflect a substitution.
-- PRECONDITION: τ is substituted.
updatePinnedTVs ∷ tv → Type tv → m ()
--
-- | Figure out which variables to generalize in a piece of syntax.
-- The 'Bool' indicates whether the syntax whose type is being
-- generalized is a syntactic value. Returns a list of
-- generalizable variables and their qualifier bounds.
generalize' ∷ Bool → Rank → Type tv → m [(tv, QLit)]
-- | Find 'QLit' bounds for a set of type variables. This assumes
-- that these variables may safely be removed from the constraint
-- if bounded as specified. In particular, all the variables must
-- appear only on the left-hand side of the qualifier inequalities.
getTVBounds ∷ [tv] → m [QLit]
-- | Ensure that the current constraint is satisfiable. This is
-- necessary after each REPL entry, because that's the commit point
-- for the constraint, and the REPL becomes unusable if a particular
-- type error hangs around in the constraint forever.
ensureSatisfiability ∷ m ()
infix 5 <:, =:, ⊏:, ~:
--
-- Pass-through instances
--
instance (MonadConstraint tv s m, Monoid w) ⇒
MonadConstraint tv s (WriterT w m) where
(<:) = lift <$$> (<:)
(=:) = lift <$$> (=:)
(⊏:) = lift <$$> (⊏:)
(~:) = lift <$$> (~:)
getPinnedTVs = lift getPinnedTVs
withPinnedTVs = mapWriterT <$> withPinnedTVs
updatePinnedTVs= lift <$$> updatePinnedTVs
generalize' = lift <$$$> generalize'
getTVBounds = lift <$> getTVBounds
ensureSatisfiability = lift ensureSatisfiability
instance MonadConstraint tv r m ⇒
MonadConstraint tv r (StateT s m) where
(<:) = lift <$$> (<:)
(=:) = lift <$$> (=:)
(⊏:) = lift <$$> (⊏:)
(~:) = lift <$$> (~:)
getPinnedTVs = lift getPinnedTVs
withPinnedTVs = mapStateT <$> withPinnedTVs
updatePinnedTVs= lift <$$> updatePinnedTVs
generalize' = lift <$$$> generalize'
getTVBounds = lift <$> getTVBounds
ensureSatisfiability = lift ensureSatisfiability
instance MonadConstraint tv p m ⇒
MonadConstraint tv p (ReaderT r m) where
(<:) = lift <$$> (<:)
(=:) = lift <$$> (=:)
(⊏:) = lift <$$> (⊏:)
(~:) = lift <$$> (~:)
getPinnedTVs = lift getPinnedTVs
withPinnedTVs = mapReaderT <$> withPinnedTVs
updatePinnedTVs= lift <$$> updatePinnedTVs
generalize' = lift <$$$> generalize'
getTVBounds = lift <$> getTVBounds
ensureSatisfiability = lift ensureSatisfiability
instance (MonadConstraint tv p m, Monoid w) ⇒
MonadConstraint tv p (RWST r w s m) where
(<:) = lift <$$> (<:)
(=:) = lift <$$> (=:)
(⊏:) = lift <$$> (⊏:)
(~:) = lift <$$> (~:)
getPinnedTVs = lift getPinnedTVs
withPinnedTVs = mapRWST <$> withPinnedTVs
updatePinnedTVs= lift <$$> updatePinnedTVs
generalize' = lift <$$$> generalize'
getTVBounds = lift <$> getTVBounds
ensureSatisfiability = lift ensureSatisfiability
--
-- Some generic operations
--
-- | Generalize a type under a constraint and environment,
-- given whether the the value restriction is satisfied or not
generalize ∷ MonadConstraint tv r m ⇒
Bool → Rank → Type tv → m (Type tv)
generalize value γrank ρ = do
αqs ← generalize' value γrank ρ
standardizeMus <$> closeQuant Forall αqs <$> subst ρ
-- | Generalize a list of types together.
generalizeList ∷ MonadConstraint tv r m ⇒
Bool → Rank → [Type tv] → m [Type tv]
generalizeList value γrank ρs = do
αqs ← generalize' value γrank (foldl tyTuple tyUnit ρs)
mapM (standardizeMus <$> closeQuant Forall αqs <$$> subst) ρs
-- | Generalize the existential type variables in a type
generalizeEx ∷ MonadConstraint tv r m ⇒
Rank → Type tv → m (Type tv)
generalizeEx γrank ρ0 = do
ρ ← subst ρ0
αs ← removeByRank γrank (filter (tvFlavorIs Existential) (ftvList ρ))
αqs ← mapM addQual αs
return (closeQuant Exists αqs ρ)
where
addQual α = case tvQual α of
Just ql → return (α, ql)
Nothing → typeBug "generalizeEx"
"existential type variable with no rank"
-- | Remove type variables from a list if their rank indicates that
-- they're in the environment or if they're pinned
removeByRank ∷ MonadConstraint tv r m ⇒ Rank → [tv] → m [tv]
removeByRank γrank αs = do
pinned ← getPinnedTVs
let keep α = do
rank ← getTVRank α
return (rank > γrank && α `S.notMember` pinned)
filterM keep αs
---
--- SUBTYPING CONSTRAINT SOLVER
---
--
-- The internal state
--
-- | The state of the constraint solver.
data CTState tv r
= CTState {
-- | Graph for subtype constraints on type variables and atomic
-- type constructors
csGraph ∷ !(Gr.Gr tv ()),
-- | Reverse lookup for turning atoms into node numbers for the
-- 'csGraph' graph
csNodeMap ∷ !(Gr.NodeMap tv),
-- | Maps type variables to same-size equivalence classes
csEquivs ∷ !(ProxyMap tv r),
-- | Types to relate by the subqualifier relation
csQuals ∷ ![(Type tv, Type tv)],
-- | Stack of pinned type variables
csPinned ∷ ![S.Set tv]
}
-- | Representation of type variable equivalence class
type TVProxy tv r = UF.Proxy r (S.Set tv)
-- | The map from type variables to equivalence classes
type ProxyMap tv r = M.Map tv (TVProxy tv r)
-- | Updater for 'csQuals' field
csQualsUpdate ∷ ([(Type tv, Type tv)] → [(Type tv, Type tv)]) →
CTState tv r → CTState tv r
csQualsUpdate f cs = cs { csQuals = f (csQuals cs) }
-- | Updater for 'csEquivs' field
csEquivsUpdate ∷ (ProxyMap tv r → ProxyMap tv r) →
CTState tv r → CTState tv r
csEquivsUpdate f cs = cs { csEquivs = f (csEquivs cs) }
-- | Updater for 'csPinned' field
csPinnedUpdate ∷ ([S.Set tv] → [S.Set tv]) →
CTState tv r → CTState tv r
csPinnedUpdate f cs = cs { csPinned = f (csPinned cs) }
instance Tv tv ⇒ Show (CTState tv r) where
showsPrec _ cs
| null (Gr.edges (csGraph cs))
, null (csQuals cs)
= id
| otherwise
= showString "CTState { csGraph = "
. shows (Gr.ShowGraph (csGraph cs))
. showString ", csQuals = "
. shows (csQuals cs)
. showString " }"
instance Tv tv ⇒ Ppr.Ppr (CTState tv r) where
ppr cs = Ppr.ppr . M.fromList $
[ ("graph", Ppr.fsep . Ppr.punctuate Ppr.comma $
[ Ppr.pprPrec 10 α1
Ppr.<> Ppr.text "<:"
Ppr.<> Ppr.pprPrec 10 α2
| (α1, α2) ← Gr.labNodeEdges (csGraph cs) ])
, ("quals", Ppr.fsep . Ppr.punctuate Ppr.comma $
[ Ppr.pprPrec 9 τ1
Ppr.<> Ppr.char '⊑'
Ppr.<> Ppr.pprPrec 9 τ2
| (τ1, τ2) ← csQuals cs
])
]
--
-- The monad transformer
--
-- | Underlying 'ConstraintT' is a monad transformer that carries merely
-- the constraint-solving state.
newtype ConstraintT_ tv r m a
= ConstraintT_ {
unConstraintT_ ∷ StateT (CTState tv r) m a
}
deriving (Functor, Applicative, Monad, MonadAlmsError, MonadTrace)
-- | Map some higher-order operation through 'ConstraintT_'.
mapConstraintT_ ∷ (∀ s. m (a, s) → n (b, s)) →
ConstraintT_ tv r m a → ConstraintT_ tv r n b
mapConstraintT_ f = ConstraintT_ . mapStateT f . unConstraintT_
-- | Constraint monad transformer carries constraint solver state.
-- 'SubstT' substitution state.
type ConstraintT tv r m = ConstraintT_ tv r (SubstT r m)
-- | Map some higher-order operation through 'ConstraintT'.
mapConstraintT ∷ (Functor m, Functor n) ⇒
(∀ s. m (a, s) → n (b, s)) →
ConstraintT tv r m a → ConstraintT tv r n b
mapConstraintT f = mapConstraintT_ (mapSubstT f')
where
f' action = unshift <$> f (shift <$> action)
shift ((a, s), s') = (a, (s, s'))
unshift (a, (s, s')) = ((a, s), s')
-- | Run the constraint solver.
runConstraintT ∷ (MonadAlmsError m, MonadRef r m) ⇒
ConstraintState (TV r) r →
ConstraintT (TV r) r m a →
m (a, ConstraintState (TV r) r)
runConstraintT ecs m = do
((result, cs), ss) ← runSubstT
(ecsSubst ecs)
(runStateT (unConstraintT_ (resetEquivTVs >> m))
(ecsInternal ecs))
return (result, ExternalConstraintState cs ss)
-- | Run a constraint computation in the IO Monad
runConstraintIO ∷ ConstraintState (TV IORef) IORef →
ConstraintT (TV IORef) IORef (AlmsErrorT IO) a →
IO (Either [AlmsError]
(a, ConstraintState (TV IORef) IORef))
runConstraintIO ecs m = runAlmsErrorT (runConstraintT ecs m)
-- | The external representation of the constraint solver's state
data ConstraintState tv r
= ExternalConstraintState {
ecsInternal ∷ !(CTState tv r),
ecsSubst ∷ !SubstState
}
-- | The initial constraint solver state
constraintState0 ∷ Tv tv ⇒ ConstraintState tv r
constraintState0
= ExternalConstraintState {
ecsInternal = CTState {
csGraph = Gr.empty,
csNodeMap = Gr.new,
csEquivs = M.empty,
csQuals = [],
csPinned = []
},
ecsSubst = substState0
}
instance Tv tv ⇒ Ppr.Ppr (ConstraintState tv r) where
ppr = Ppr.ppr . ecsInternal
instance Tv tv ⇒ Show (ConstraintState tv r) where
showsPrec = Ppr.showFromPpr
-- | Get a printable representations of the internal constraint-solving
-- state.
pprConstraintState ∷ Tv tv ⇒ ConstraintState tv r → Ppr.Doc
pprConstraintState = Ppr.ppr . ecsInternal
--
-- Instances
--
-- | Transformer instance
instance MonadTrans (ConstraintT_ tv r) where
lift = ConstraintT_ . lift
-- | Pass through for reference operations
instance MonadSubst tv r m ⇒
MonadRef r (ConstraintT_ tv r m) where
newRef = lift <$> newRef
readRef = lift <$> readRef
writeRef = lift <$$> writeRef
-- | Pass through for unification operations
instance MonadSubst tv r m ⇒
MonadSubst tv r (ConstraintT_ tv r m) where
newTV_ (Universal, kind, bound, descr) = do
α ← lift (newTV' (kind, descr))
fvTy α ⊏: bound
return α
newTV_ attrs = lift (newTV' attrs)
writeTV_ = lift <$$> writeTV_
readTV_ = lift <$> readTV_
getTVRank_ = lift <$> getTVRank_
setTVRank_ = lift <$$> setTVRank_
collectTVs = mapConstraintT_ (mapListen2 collectTVs)
reportTVs = lift . reportTVs
monitorChange = mapConstraintT_ (mapListen2 monitorChange)
setChanged = lift setChanged
-- | 'ConstraintT' implements 'Graph'/'NodeMap' transformer operations
-- for accessing its graph and node map.
instance (Ord tv, Monad m) ⇒
Gr.MonadNM tv () Gr.Gr (ConstraintT_ tv r m) where
getNMState = ConstraintT_ (gets (csNodeMap &&& csGraph))
getNodeMap = ConstraintT_ (gets csNodeMap)
getGraph = ConstraintT_ (gets csGraph)
putNMState (nm, g) = ConstraintT_ . modify $ \cs →
cs { csNodeMap = nm, csGraph = g }
putNodeMap nm = ConstraintT_ . modify $ \cs → cs { csNodeMap = nm }
putGraph g = ConstraintT_ . modify $ \cs → cs { csGraph = g }
-- | Constraint solver implementation.
instance MonadSubst tv r m ⇒
MonadConstraint tv r (ConstraintT_ tv r m) where
τ <: τ' = do
traceN 3 ("<:", τ, τ')
runSeenT (subtypeTypes False τ τ')
τ =: τ' = do
traceN 3 ("=:", τ, τ')
runSeenT (subtypeTypes True τ τ')
τ ⊏: τ' = do
traceN 3 ("⊏:", qualToType τ, qualToType τ')
addQualConstraint τ τ'
--
getPinnedTVs = S.unions <$> ConstraintT_ (gets csPinned)
--
withPinnedTVs a m = do
let αs = ftvSet a
ConstraintT_ (modify (csPinnedUpdate (αs :)))
result ← m
ConstraintT_ (modify (csPinnedUpdate tail))
return result
--
updatePinnedTVs α τ = do
let βs = ftvSet τ
update = snd . mapAccumR eachSet False
eachSet False set
| α `S.member` set = (True, βs `S.union` S.delete α set)
eachSet done set = (done, set)
ConstraintT_ (modify (csPinnedUpdate update))
--
generalize' = solveConstraint
getTVBounds = solveBounds
ensureSatisfiability = checkQualifiers
{-# INLINE gtraceN #-}
gtraceN ∷ (TraceMessage a, Tv tv, MonadTrace m) ⇒
Int → a → ConstraintT_ tv r m ()
gtraceN =
if debug then \n info →
if n <= debugLevel then do
trace info
cs ← ConstraintT_ get
let doc = Ppr.ppr cs
unless (Ppr.isEmpty doc) $
trace (Ppr.nest 4 doc)
else return ()
else \_ _ → return ()
-- | Monad transformer for tracking which type comparisons we've seen,
-- in order to implement recursive subtyping. A pair of types mapped
-- to @True@ means that they're known to be equal, whereas @False@
-- means that they're only known to be subtyped.
type SeenT tv r m = StateT (M.Map (Type tv, Type tv) Bool)
(ConstraintT_ tv r m)
-- | Run a recursive subtyping computation.
runSeenT ∷ (Tv tv, MonadTrace m) ⇒ SeenT tv r m a → ConstraintT_ tv r m a
runSeenT m = do
gtraceN 4 "runSeenT {"
result ← evalStateT m M.empty
gtraceN 4 "} runSeenT"
return result
-- | Relate two types at either subtyping or equality, depending on
-- the value of the first parameter (@True@ means equality).
-- This eagerly solves as much as possible, adding to the constraint
-- only as necessary.
subtypeTypes ∷ MonadSubst tv r m ⇒
Bool → Type tv → Type tv → SeenT tv r m ()
subtypeTypes unify = check where
check τ1 τ2 = do
lift $ gtraceN 4 ("subtypeTypes", unify, τ1, τ2)
τ1' ← subst τ1
τ2' ← subst τ2
seen ← get
unless (M.lookup (τ1', τ2') seen >= Just unify) $ do
put (M.insert (τ1', τ2') unify seen)
decomp τ1' τ2'
--
decomp τ1 τ2 = case (τ1, τ2) of
(TyVar v1, TyVar v2)
| v1 == v2 → return ()
(TyVar (Free r1), TyVar (Free r2))
| tvFlavorIs Universal r1, tvFlavorIs Universal r2 →
if unify
then unifyVar r1 (fvTy r2)
else do
lift (makeEquivTVs r1 r2)
addEdge r1 r2
(TyVar (Free r1), _)
| tvFlavorIs Universal r1 →
occursCheck r1 τ2 decomp $ \τ2'' → do
τ2' ← if unify then return τ2'' else copyType τ2''
unifyVar r1 τ2'
unless unify (check τ2' τ2)
(_, TyVar (Free r2))
| tvFlavorIs Universal r2 → do
occursCheck r2 τ1 (flip decomp) $ \τ1'' → do
τ1' ← if unify then return τ1'' else copyType τ1''
unifyVar r2 τ1'
unless unify (check τ1 τ1')
(TyQu Forall αs1 τ1', TyQu Forall αs2 τ2')
| if unify
then αs1 == αs2
else length αs1 == length αs2
&& and (zipWith ((⊒)`on`snd) αs1 αs2) →
check τ1' τ2'
(TyQu Exists αs1 τ1', TyQu Exists αs2 τ2')
| αs1 == αs2 →
check τ1' τ2'
(TyApp tc1 τs1, TyApp tc2 τs2)
| tc1 == tc2 && tc1 /= tcRowMap && length τs1 == length τs2 →
sequence_
[ if unify
then if isQVariance var
then τ1' ~: τ2'
else check τ1' τ2'
else relateTypes var τ1' τ2'
| var ← tcArity tc1
| τ1' ← τs1
| τ2' ← τs2 ]
(TyRow n1 τ11 τ12, TyRow n2 τ21 τ22)
| n1 == n2 → do
check τ11 τ21
check τ12 τ22
| otherwise → do
α ← newTVTy
check (TyRow n1 τ11 α) τ22
β ← newTVTy
check τ12 (TyRow n2 τ21 β)
check α β
(TyMu _ τ1', _) →
decomp (openTy 0 [τ1] τ1') τ2
(_, TyMu _ τ2') →
decomp τ1 (openTy 0 [τ2] τ2')
_ | Just (τ1', τ2') ← matchReduce τ1 τ2 →
check τ1' τ2'
(TyApp tc1 [τ11, τ12], TyApp tc2 [τ21, τ22])
| tc1 == tcRowMap && tc2 == tcRowMap → do
check τ11 τ21
check τ12 τ22
_ | otherwise →
tErrExp
(if unify
then [msg| Cannot unify: |]
else [msg| Cannot subtype: |])
(pprMsg τ1)
(pprMsg τ2)
--
addEdge a1 a2 = do
Gr.insNewMapNodeM a1
Gr.insNewMapNodeM a2
Gr.insMapEdgeM (a1, a2, ())
lift (fvTy a1 ⊏: fvTy a2)
-- | Relate two types at the given variance.
relateTypes ∷ MonadSubst tv r m ⇒
Variance → Type tv → Type tv → SeenT tv r m ()
relateTypes var = case var of
Invariant → subtypeTypes True
Covariant → subtypeTypes False
Contravariant → flip (subtypeTypes False)
QInvariant → (~:)
QCovariant → (⊏:)
QContravariant→ flip (⊏:)
Omnivariant → \_ _ → return ()
-- | Copy a type while replacing all the type variables with fresh ones
-- of the same kind.
copyType ∷ MonadSubst tv r m ⇒ Type tv → m (Type tv)
copyType =
foldTypeM (mkQuF (return <$$$> TyQu))
(mkBvF (return <$$$> bvTy))
fvar
fcon
(return <$$$> TyRow)
(mkMuF (return <$$> TyMu))
where
fvar α | tvFlavorIs Universal α = newTVTy' (tvKind α)
| otherwise = return (fvTy α)
-- Nullary type constructors that are involved in the atomic subtype
-- relation are converted to type variables:
fcon tc τs
= TyApp tc <$> sequence
[ -- A Q-variant type constructor parameter becomes a single
-- type variable:
if isQVariance var
then newTVTy' KdQual
else return τ
| τ ← τs
| var ← tcArity tc ]
-- | Unify a type variable with a type, where the type must be locally
-- closed.
-- ASSUMPTIONS: @α@ has not been substituted and the occurs check has
-- already passed.
unifyVar ∷ MonadSubst tv r m ⇒ tv → Type tv → SeenT tv r m ()
unifyVar α τ0 = do
lift $ gtraceN 4 ("unifyVar", α, τ0)
τ ← subst τ0
tassert (lcTy 0 τ)
[msg|
Cannot unify because a $τ is insufficiently polymorphic
|]
writeTV α τ
lift (updatePinnedTVs α τ)
(n, _) ← Gr.mkNodeM α
gr ← Gr.getGraph
case Gr.match n gr of
(Nothing, _) → return ()
(Just (pres, _, _, sucs), gr') → do
Gr.putGraph gr'
sequence_ $
[ case Gr.lab gr' n' of
Nothing → return ()
Just a → subtypeTypes False (fvTy a) τ
| (_, n') ← pres ]
++
[ case Gr.lab gr' n' of
Nothing → return ()
Just a → subtypeTypes False τ (fvTy a)
| (_, n') ← sucs ]
--- OCCURS CHECK
-- | Performs the occurs check and returns a type suitable for unifying
-- with the given type variable, if possible. This does the subtyping
-- occurs check, which checks not in terms of type variables but in
-- terms of same-size equivalence classes of type variables.
-- Unification is possible if all occurrences of type variables
-- size-equivalent to @α@ appear guarded by a type constructor that
-- permits recursion, in which case we roll up @τ@ as a recursive type
-- and return that.
occursCheck ∷ MonadSubst tv r m ⇒
tv → Type tv →
(Type tv → Type tv → SeenT tv r m ()) →
(Type tv → SeenT tv r m ()) →
SeenT tv r m ()
occursCheck α τ0 kv kt = do
lift (gtraceN 3 ("occursCheck", α, τ0))
loop S.empty τ0
where
loop seen τ = do
let (guarded, unguarded) = (M.keys***M.keys) . M.partition id $ ftvG τ
apparentCycle ← lift $ anyA (checkEquivTVs α) unguarded
if apparentCycle
then case headReduceType τ of
Next τ'@(TyVar (Free _)) → kv (fvTy α) τ'
Next τ' | τ' ∉ seen → loop (S.insert τ' seen) τ'
_ →
-- | This type error has to throw because continuing will
-- likely cause the type checker to diverge.
typeError' [msg|
Occurs check failed.
Cannot construct an infinite type when unifying:
<dl>
<dt>type variable <dd>$α
<dt>type <dd>$τ0
</dl>
|]
else do
recVars ← lift $ filterM (checkEquivTVs α) guarded
unless (null recVars) $
lift (gtraceN 3 ("occursCheck", "recvars", recVars))
kt (foldr closeRec τ recVars)
-- | Records that two type variables have the same size.
makeEquivTVs ∷ MonadSubst tv r m ⇒ tv → tv → ConstraintT_ tv r m ()
makeEquivTVs α β = do
pα ← getTVProxy α
pβ ← getTVProxy β
UF.coalesce_ (return <$$> S.union) pα pβ
-- | Checks whether two type variables have the same size.
checkEquivTVs ∷ MonadSubst tv r m ⇒ tv → tv → ConstraintT_ tv r m Bool
checkEquivTVs α β = do
pα ← getTVProxy α
pβ ← getTVProxy β
UF.sameRepr pα pβ
-- | Clears all size-equivalence classes and rebuilds them based on the
-- current atomic subtyping constraint graph.
resetEquivTVs ∷ MonadSubst tv r m ⇒ ConstraintT_ tv r m ()
resetEquivTVs = do
ConstraintT_ (modify (csEquivsUpdate (const M.empty)))
g ← Gr.getGraph
mapM_ (uncurry makeEquivTVs)
[ (α, β) | (α, β) ← Gr.labNodeEdges g ]
-- | Helper to get the proxy the represents the size-equivalence class
-- of a type variable.
getTVProxy ∷ MonadSubst tv r m ⇒ tv → ConstraintT_ tv r m (TVProxy tv r)
getTVProxy α = do
equivs ← ConstraintT_ (gets csEquivs)
case M.lookup α equivs of
Just pα → return pα
Nothing → do
pα ← UF.create (S.singleton α)
ConstraintT_ (modify (csEquivsUpdate (M.insert α pα)))
return pα
--- CONSTRAINT SOLVING
-- | Solve a constraint as much as possible, returning the type
-- variables to generalize and their qualifier bounds.
solveConstraint ∷ MonadSubst tv r m ⇒
Bool → Rank → Type tv → ConstraintT_ tv r m [(tv, QLit)]
solveConstraint value γrank τ0 = do
τ ← subst τ0
let τftv = ftvV τ
gtraceN 2 (TraceIn ("gen", "begin", value, γrank, τftv, τ))
τftv ← coalesceSCCs τftv
gtraceN 3 ("gen", "scc", τftv, τ)
Gr.modifyGraph Gr.trcnr
gtraceN 4 ("gen", "trc", τftv, τ)
eliminateExistentials True (γrank, τftv)
gtraceN 3 ("gen", "existentials 1", τftv, τ)
untransitive
gtraceN 3 ("gen", "untrans", τftv, τ)
eliminateExistentials False (γrank, τftv)
gtraceN 3 ("gen", "existentials 2", τftv, τ)
τftv ← polarizedReduce τftv
gtraceN 3 ("gen", "polarized", τftv, τ)
eliminateExistentials False (γrank, τftv)
gtraceN 3 ("gen", "existentials 3", τftv, τ)
-- Guessing starts here
τftv ← coalesceComponents value (γrank, τftv)
gtraceN 3 ("gen", "components", τftv, τ)
-- Guessing ends here
qc ← ConstraintT_ $ gets csQuals >>= mapM subst
cftv ← S.fromList . map snd <$> Gr.getsGraph Gr.labNodes
αs ← S.fromDistinctAscList <$>
filter (tvFlavorIs Universal) <$>
(removeByRank γrank
(S.toAscList $ (ftvSet qc `S.union` M.keysSet τftv) S.\\ cftv))
(qc, αqs, τ) ← solveQualifiers value αs qc τ
ConstraintT_ (modify (csQualsUpdate (const qc)))
gtraceN 2 (TraceOut ("gen", "finished", αqs, τ))
resetEquivTVs
return αqs
where
--
-- Eliminate existentially-quantified type variables from the
-- constraint
eliminateExistentials trans (γrank, τftv) = do
extvs ← getExistentials (γrank, τftv)
traceN 4 ("existentials:", extvs)
mapM (eliminateNode trans) (S.toList extvs)
-- Get the existential type variables
getExistentials (γrank, τftv) = do
lnodes ← Gr.getsGraph Gr.labNodes
cftv ← removeByRank γrank [ α | (_, α) ← lnodes ]
return (S.fromList cftv S.\\ M.keysSet τftv)
-- Remove a node unless it is necessary to associate some of its
-- neighbors -- in particular, a node with multiple predecessors
-- but no successor (or dually, multiple successors but no
-- predecessor) should not be removed.
eliminateNode trans α = do
(nm, g) ← Gr.getNMState
let node = Gr.nmLab nm α
case (Gr.pre g node, Gr.suc g node) of
(_:_:_, []) → return ()
([], _:_:_) → return ()
(pre, suc) → do
β ← newTVTy' KdQual
writeTV α β
traceN 4 ("eliminateNode",
catMaybes (map (Gr.lab g) pre),
β,
catMaybes (map (Gr.lab g) suc))
Gr.putGraph $
let g' = Gr.delNode node g in
if trans
then g'
else foldr ($) g'
[ Gr.insEdge (n1, n2, ())
| n1 ← pre
, n2 ← suc ]
--
-- Remove redundant edges:
-- • Edges implied by transitivity
untransitive = Gr.modifyGraph Gr.untransitive
--
-- Remove type variables based on polarity-related rules:
-- • Coalesce positive type variables with a single predecessor
-- and negative type variables with a single successor
-- • Coalesce positive type variables that share all their
-- predecessors and negative type variables that share all
-- their successors.
polarizedReduce = iterChanging $ \τftv → do
nm ← Gr.getNodeMap
foldM tryRemove τftv (findPolar nm τftv)
where
tryRemove τftv (n, α, var) = do
let ln = (n, α)
mτ ← readTV α
g ← Gr.getGraph
case (mτ, Gr.gelem n g) of
(Left _, True) →
case (var, Gr.pre g n, Gr.suc g n) of
-- Should we consider QCo(ntra)variance here too?
(Covariant, [pre], _)
→ snd <$> coalesce ln (Gr.labelNode g pre) τftv
(Contravariant, _, [suc])
→ snd <$> coalesce ln (Gr.labelNode g suc) τftv
(Covariant, pres, _)
→ siblings g τftv (ln, 1) pres (Gr.pre,Gr.suc)
(Contravariant, _, sucs)
→ siblings g τftv (ln, -1) sucs (Gr.suc,Gr.pre)
_ → return τftv
_ → return τftv
findPolar nm τftv = [ (Gr.nmLab nm α, α, var)
| (α, var) ← M.toList τftv
, var == 1 || var == -1 ]
siblings g τftv (lnode@(n,_), var) pres (gpre, gsuc) = do
lnodes ← liftM ordNub . runListT $ do
pre ← ListT (return pres)
sib ← ListT (return (gsuc g pre))
guard $ sib /= n
Just β ← return (Gr.lab g sib)
guard $ M.lookup β τftv == Just var
guard $ gpre g sib == pres
return (sib, β)
case lnodes of
_:_ → do
τftv' ← snd <$> coalesceList τftv (lnode:lnodes)
return τftv'
_ → return τftv
--
-- Coalesce the strongly-connected components to single atoms
coalesceSCCs τftv = do
foldM (liftM snd <$$> coalesceList) τftv =<< Gr.getsGraph Gr.labScc
-- Given a list of atoms, coalesce them to one atom
coalesceList τftv0 (ln:lns) =
foldM (\(ln1, state) ln2 → coalesce ln1 ln2 state) (ln, τftv0) lns
coalesceList _ [] = typeBug "coalesceList" "Got []"
-- Assign n2 to n1, updating the graph, type variables, and ftvs,
-- and return whichever node survives
-- PRECONDITION: α1 /= α2
coalesce (n1, α1) (n2, α2) τftv = do
τftv' ← assignTV α1 α2 τftv
assignNode n1 n2
return ((n2, α2), τftv')
-- Update the graph to remove node n1, assigning all of its
-- neighbors to n2
assignNode n1 n2 = Gr.modifyGraph $ \g →
Gr.insEdges [ (n', n2, ())
| n' ← Gr.pre g n1, n' /= n1, n' /= n2 ] $
Gr.insEdges [ (n2, n', ())
| n' ← Gr.suc g n1, n' /= n1, n' /= n2 ] $
Gr.delNode n1 g
-- Update the type variables to assign β to α, updating the
-- ftvs appropriately
assignTV α β τftv = do
writeTV α (fvTy β)
updatePinnedTVs α (fvTy β)
assignFtvMap α β τftv
-- Given two type variables, where α ← β, update a map of free
-- type variables to variance lists accordingly
assignFtvMap α β vmap =
case M.lookup α vmap of
Just vs → return $ M.insertWith (+) β vs vmap'
Nothing → return vmap
where vmap' = M.delete α vmap
-- Coalesce and remove fully-generalizable components
coalesceComponents value (γrank, τftv) = do
extvs ← getExistentials (γrank, τftv)
τcands ← genCandidates value τftv γrank
let candidates = extvs `S.union` τcands
each τftv component@(_:_)
| all (`S.member` candidates) (map snd component)
= do
((node, _), τftv')
← coalesceList τftv component
Gr.getGraph >>= Gr.putGraph . Gr.delNode node
return τftv'
each τftv _
= return τftv
foldM each τftv =<< Gr.getsGraph Gr.labComponents
-- Find the generalization candidates, which are free in τ but
-- not in γ (restricted further if not a value)
genCandidates value τftv γrank =
S.fromDistinctAscList <$>
removeByRank γrank (map fst (M.toAscList (restrict τftv)))
where
restrict = if value
then id
else M.filter (`elem` [1, -1, 2, -2])
---
--- QUALIFIER CONSTRAINT SOLVING
---
{-
Syntactic metavariables:
γ: any type variable
α: generalization candidates
β: type variables with Q-variance
δ: generalization candidates with Q-variance
q: qualifier literals
_s: a collection of _
qe ::= q | γs | q γs (qualifier expressions)
First rewrite as follows:
(DECOMPOSE)
γs₁ \ γs₂ = γ₁ ... γⱼ
βs = { γ ∈ γs₂ | γ is Q-variant }
βsᵢ = if γᵢ is Q-variant then γs₂ else βs
-----------------------------------------------------------------------
q₁ γs₁ ⊑ q₂ γs₂ ---> q₁ \-\ q₂ ⊑ βs ⋀ γ₁ ⊑ q₁ βs₁ ⋀ ... ⋀ γⱼ ⊑ q₁ βsᵢ
(BOT-SAT)
---------------
U ⊑ βs ---> ⊤
(TOP-SAT)
-----------------
γ ⊑ A βs ---> ⊤
(BOT-UNSAT)
q ≠ U
-----------------
q ⊑ U ---> fail
(COMBINE-QLIT)
--------------------------------------------
γ ⊑ q ⋀ γ ⊑ q' ⋀ C; τ ---> γ ⊑ q⊓q' ⋀ C; τ
(COMBINE-LE)
q ⊑ q' βs ⊆ βs'
---------------------------------------------------
γ ⊑ q βs ⋀ γ ⊑ q' βs' ⋀ C; τ ---> γ ⊑ q βs ⋀ C; τ
Then we have a constraint where each inequality is in one of two forms:
γ ⊑ q βs
q ⊑ βs
Now we continue to rewrite and perform substitutions as well. Continue
to apply the above rules when they apply. These new rewrites apply to a
whole constraint and type together, not to single atomic constraints.
For a type variable γ and type τ, let V(γ,τ) be γ's variance in τ. We
also refer to the free type variables in only the lower or upper bounds
of a constraint C as lftv(C) and uftv(C), respectively.
These are non-lossy rewrites. Repeat them as much as possible,
continuing to apply the rewrites above when applicable:
(FORCE-U)
-------------------------------
β ⊑ U ⋀ C; τ ---> [U/β](C; τ)
(SUBST-NEG)
δ ∉ lftv(C) V(δ,τ) ⊑ Q-
---------------------------------
δ ⊑ qe ⋀ C; τ ---> [qe/δ](C; τ)
(SUBST-NEG-TOP)
δ ∉ lftv(C) V(δ,τ) ⊑ Q-
-------------------------
C; τ ---> [A/δ](C; τ)
(SUBST-POS)
δ ∉ uftv(C) V(δ,τ) ⊑ Q+
-----------------------------------------------------------
qe₁ ⊑ δ ⋀ ... ⋀ qeⱼ ⊑ δ ⋀ C; τ ---> [qe₁⊔...⊔qeⱼ/δ](C; τ)
(SUBST-INV)
δ ∉ uftv(C) V(δ,τ) = Q= δ' fresh
--------------------------------------------------------------
qe₀ ⊑ δ ⋀ ... ⋀ qeⱼ ⊑ δ ⋀ C; τ ---> [δ'⊔qe₀⊔...⊔qeⱼ/δ](C; τ)
Substitute for contravariant qualifier variables by adding these lossy
rewrites:
(SUBST-NEG-LOSSY)
δ ∉ lftv(C) V(δ,τ) = Q-
-----------------------------------------------
δ ⊑ q₁ βs₁ ⋀ ... ⋀ δ ⊑ qⱼ βsⱼ ⋀ C; τ
---> [(q₁⊓...⊓qⱼ) (βs₁ ∩ ... ∩ βsⱼ)/δ](C; τ)
Run SAT as below for anything we missed. Then, add bounds:
(BOUND)
α ∉ lftv(C) V(α,τ) ∈ { -, +, =, Q= } q = q₁⊓...⊓qⱼ
------------------------------------------------------
α ⊑ q₁ βs₁ ⋀ ... ⋀ α ⊑ qⱼ βsⱼ ⋀ C; τ
---> [U/α]C; ∀α:q. τ
We convert it to SAT as follows:
Define:
πa(Q) = A ⊑ Q
πa(β) = 2 * tvId β + 1
πa(q1 ⊔ q2) = πa(q1) ⋁ πa(q2)
πa(q1 ⊓ q2) = πa(q1) ⋀ πa(q2)
Then given the constraint
q1 ⊑ q1' ⋀ ... ⋀ qk ⊑ qk'
generate the formula:
(πa(q1) ⇒ πa(q1'))
⋀ ... ⋀
(πa(qk) ⇒ πa(qk'))
-}
-- | Represents the meet of several qualifier expressions, which happens
-- when some variable has multiple upper bounds. These are normalized
-- to implement COMBINE-QLIT and COMBINE-LE.
newtype QEMeet tv = QEMeet { unQEMeet ∷ [S.Set tv] }
instance Bounded (QEMeet tv) where
minBound = QEMeet [S.empty]
maxBound = QEMeet []
instance Tv tv ⇒ Ppr.Ppr (QEMeet tv) where
ppr (QEMeet []) = Ppr.char 'A'
ppr (QEMeet [qe]) = Ppr.ppr (QeU qe)
ppr (QEMeet qem) =
Ppr.prec Ppr.precCaret $
Ppr.fsep (Ppr.punctuate (Ppr.text " ⋀")
(Ppr.ppr <$> QeU <$> qem))
instance Tv tv ⇒ Show (QEMeet tv) where showsPrec = Ppr.showFromPpr
instance Ord tv ⇒ Ftv (QEMeet tv) tv where
ftvTree = FTBranch . map FTSingle . S.toList . ftvSet
ftvSet = S.unions . unQEMeet
instance Ord tv ⇒ Monoid (QEMeet tv) where
mempty = maxBound
mappend = foldr (qemInsert . QeU) <$.> unQEMeet
qemSingleton ∷ QExp tv → QEMeet tv
qemSingleton QeA = maxBound
qemSingleton (QeU αs) = QEMeet [αs]
qemInsert ∷ Ord tv ⇒ QExp tv → QEMeet tv → QEMeet tv
qemInsert qe (QEMeet qem) = QEMeet (loop qe qem) where
loop QeA qem = qem
loop (QeU αs) qem = loopU αs qem
loopU αs [] = [αs]
loopU αs (βs:qem)
| αs `S.isSubsetOf` βs = loopU αs qem
| βs `S.isSubsetOf` αs = βs:qem
| otherwise = βs:loopU αs qem
-- | State of the qualifier constraint solver
data QCState tv
= QCState {
-- | Generalization candidates, which are type variables that
-- appear in the qualifier constraint or type-to-be-generalized,
-- but not in the shape constraint or environment
sq_αs ∷ !(S.Set tv),
-- | The current type to be generalized
sq_τ ∷ !(Type tv),
-- | Free type variables and variances in the type-to-be-generalized.
sq_τftv ∷ !(VarMap tv),
-- | Part of the qualifier constraint: joins of type variables
-- lower-bounded by qualifier literals.
sq_βlst ∷ ![(QLit, S.Set tv)],
-- | Part of the qualifier constraint: type variables
-- upper-bounded by (meets of) qualifier expressions.
sq_vmap ∷ !(M.Map tv (QEMeet tv))
}
deriving Show
-- | The empty qualifier constraint
qcState0 ∷ QCState tv
qcState0 = QCState S.empty tyUnit M.empty mempty M.empty
instance Tv tv ⇒ Ppr.Ppr (QCState tv) where
ppr sq = p . M.fromList $
[ ("αs", p (sq_αs sq))
, ("τ", p (sq_τ sq))
, ("τftv", p (sq_τftv sq))
, ("βlst", Ppr.fsep . Ppr.punctuate (Ppr.text " ⋀") $
[ p ql Ppr.<> Ppr.char '⊑' Ppr.<>
Ppr.hcat (Ppr.punctuate (Ppr.char '⊔')
(p <$> S.toList tvs))
| (ql, tvs) ← sq_βlst sq ])
, ("vmap", Ppr.fsep . Ppr.punctuate (Ppr.text " ⋀") $
[ p α Ppr.<> Ppr.char '⊑' Ppr.<> p qe
| (α, qem) ← M.toList (sq_vmap sq)
, qe ← unQEMeet qem ])
]
where p x = Ppr.ppr x
---
--- MAIN QUALIFIER CONSTRAINT OPERATIONS
---
-- | Add a qualifier subtyping constraint
addQualConstraint ∷ (MonadSubst tv r m, Qualifier q1 tv, Qualifier q2 tv) ⇒
q1 → q2 → ConstraintT_ tv r m ()
addQualConstraint q1 q2 = do
q1' ← simplifyQual q1
q2' ← simplifyQual q2
tassert (q1' /= qlitexp Qa || q2' /= qlitexp Qu)
[msg| Qualifier inequality unsatisfiable: Attempted to use an
affine type where only an unlimited type is permitted. |]
let qe1 = mapQExp (S.mapMonotonic Free) q1'
qe2 = mapQExp (S.mapMonotonic Free) q2'
unless (q1' ⊑ q2') $
ConstraintT_ . modify . csQualsUpdate $
((qualToType qe1, qualToType qe2) :)
-- Find qualifier bounds for type variables that definitely have only
-- upper bounds.
solveBounds ∷ MonadSubst tv r m ⇒
[tv] → ConstraintT_ tv r m [QLit]
solveBounds αs = do
qc ← ConstraintT_ (gets csQuals)
state ← decomposeQuals qc qcState0
traceN 4 ("solveBounds", "decompose", state)
let vmap = sq_vmap state
ConstraintT_ . modify . csQualsUpdate . const $
recomposeQuals state { sq_vmap = foldl' (flip M.delete) vmap αs }
return [ case M.lookup α vmap of
Just (QEMeet (_:_)) → Qu
_ → Qa
| α ← αs ]
-- Ensure that the qualifier constraint is satisfiable, but don't
-- make any approximating assumptions toward solving the constraint.
checkQualifiers ∷ MonadSubst tv r m ⇒ ConstraintT_ tv r m ()
checkQualifiers = do
qc ← ConstraintT_ (gets csQuals)
state ← decomposeQuals qc qcState0
traceN 4 ("checkQualifiers", "decompose", state)
runSat state False
ConstraintT_ . modify . csQualsUpdate . const $ recomposeQuals state
-- | Solver for qualifier contraints.
-- Given a qualifier constraint, solve and produce type variable
-- bounds. Also return any remaining inequalities (which must be
-- satisfiable, but we haven't guessed how to satisfy them yet).
solveQualifiers
∷ MonadConstraint tv r m ⇒
-- | Are we generalizing the type of a non-expansive term?
Bool →
-- | Generalization candidates
S.Set tv →
-- | The constraint as pairs of types in the subqualifier relation
[(Type tv, Type tv)] →
-- | The type to be generalized
Type tv →
m ([(Type tv, Type tv)], [(tv, QLit)], Type tv)
solveQualifiers value αs qc τ = do
traceN 3 (TraceIn ("solveQ", "init", αs, qc))
-- Decompose implements DECOMPOSE, TOP-SAT, BOT-SAT, and BOT-UNSAT.
τftv ← ftvV <$> subst τ
state ← decomposeQuals qc qcState0 {
sq_αs = αs,
sq_τftv = τftv,
sq_τ = τ
}
traceN 4 ("solveQ", "decompose", state)
-- Rewrite until it stops changing
state ← iterChanging
(stdizeType >=>
forceU >=>
substNeg False >=>!
substPosInv >=>!
substNeg True)
state
traceN 4 ("solveQ", "rewrites", state)
-- Try the SAT solver, then recheck
state ← runSat state True
traceN 4 ("solveQ", "sat", state)
runSat state False
-- Finish by reconstructing the constraint and returning the bounds
-- for the variables to quantify.
state ← genVars state
traceN 3 (TraceOut ("solveQ", "done", state))
return (recomposeQuals state, getBounds state, τ)
where
--
-- Standardize the qualifiers in the type
stdizeType state = do
τ ← subst τ
let meet (QEMeet [αs])
| S.null αs = Qu
meet _ = Qa
qm = meet <$> sq_vmap state
τ' = standardizeQuals qm τ
τftv = ftvV τ'
traceN 5 ("stdizeType", τ, τ', qm)
return state {
sq_τ = τ',
sq_τftv = τftv
}
--
-- Substitute U for qualifier variables upper bounded by U (FORCE-U).
forceU state =
qSubsts "forceU" state $
minBound <$
M.filterWithKey
(\β qem → case qem of
QEMeet [γs] → qUnifiable state β && S.null γs
_ → False)
(sq_vmap state)
--
-- Replace Q- and 0-variant variables by a single upper bound, if they
-- have only one (SUBST-NEG), or by A if they have none (SUBST-NEG-TOP).
-- If 'doLossy', then we include SUBST-NEG-LOSSY as well, which uses
-- approximate lower bounds for combining multiple upper bounds.
substNeg doLossy state =
qSubsts who state $ M.fromDistinctAscList $ do
δ ← S.toAscList (sq_αs state)
guard (qUnifiable state δ
&& M.lookup δ (sq_τftv state) ⊑ Just QContravariant)
case M.lookup δ (sq_vmap state) of
Nothing → return (δ, maxBound)
Just (QEMeet []) → return (δ, maxBound)
Just (QEMeet [qe]) → return (δ, QeU qe)
Just (QEMeet qes)
| doLossy → return (δ, bigMeet (QeU <$> qes))
| otherwise → mzero
where who = if doLossy then "substNeg/lossy" else "substNeg"
--
-- Replace Q+ and Q= variables with tight lower bounds.
substPosInv state = do
let add qe (S.toList → [β])
| β `S.member` sq_αs state
= M.insertWith (liftA2 (⊔)) β (Just qe)
add _ βs
= M.union (setToMap Nothing βs)
-- For each (γ ⊑ meet) in the state, make γ ⊑ each qe in the meet
add_vmap = M.foldrWithKey each <-> (sq_vmap state) where
each γ (QEMeet qem) = foldr (add (qvarexp γ)) <-> qem
-- for each (q ⊑ βs) in the state, make q ⊑ βs
add_βlst = foldr each <-> sq_βlst state where
each (q, βs) = add (qlitexp q) βs
-- The lower bounds
lbs = M.mapMaybe id . add_βlst . add_vmap
$ setToMap (Just minBound)
(S.filter (qUnifiable state) (sq_αs state))
M.\\ sq_vmap state
-- Positive variables with lower bounds
pos = lbs M.\\ M.filter (/= QCovariant) (sq_τftv state)
-- Invariant variables with lower bounds
inv = lbs `M.intersection`
M.filter (== QInvariant) (sq_τftv state)
(δ's, inv) ← first S.fromDistinctAscList . unzip <$> sequence
[ do
δ' ← newTV' KdQual
return (δ', (δ, S.insert δ' `mapQExp` qe))
| (δ, qe) ← M.toAscList inv
, qe /= minBound ]
qSubsts "substPosInv"
state {
sq_αs = sq_αs state `S.union` δ's
}
(pos `M.union` M.fromDistinctAscList inv)
--
-- Find the variables to generalize
genVars state = return state { sq_αs = αs' } where
αs' = sq_αs state `S.intersection` kset
kset = M.keysSet (keep (sq_τftv state))
keep = if value then id else M.filter (`elem` [-2,-1,1,2])
--
-- Find the the bounds of variables to generalize
getBounds state =
map (id &&& getBound) (S.toList (sq_αs state)) where
getBound α = maybe maxBound qeMeetQLit (M.lookup α (sq_vmap state))
--
-- The QLit lower bound of a QExp
qeMeetQLit (QEMeet []) = maxBound
qeMeetQLit _ = minBound
---
--- COMMON QUALIFIER CONSTRAINT HELPERS
---
-- Put a set of qualifier inequalities in decomposed form (given
-- possibly some in decomposed form already.
decomposeQuals ∷ MonadSubst tv r m ⇒
[(Type tv, Type tv)] →
QCState tv →
m (QCState tv)
decomposeQuals qc0 state0 = do
qc ← stdize qc0
traceN 4 ("decomposeQuals", "stdize", qc)
decompose state0 qc
where
--
-- Given a list of qualifier inequalities on types, produce a list of
-- inequalities on standard-form qualifiers, omitting trivial
-- inequalities along the way.
stdize qc = mapM each qc where
each (τl, τh) = do
qe1 ← simplifyQual τl
qe2 ← simplifyQual τh
return (qe1, qe2)
--
-- Given a list of inequalities on qualifiers, rewrite them into
-- the two decomposed forms:
--
-- • γ ⊑ q βs
--
-- • q ⊑ βs
--
-- This implements DECOMPOSE, BOT-SAT, TOP-SAT, and BOT-UNSAT.
decompose = foldM each where
each state (_, QeA) = return state -- (TOP-SAT)
each state (QeA, QeU γs2) = each' state (Qa, S.empty) γs2
each state (QeU γs1, QeU γs2) = each' state (Qu, γs1) γs2
each' state (q1, γs1) γs2 = do
let γs' = γs1 S.\\ γs2
βs' = S.filter flex γs2
flex = (||) <$> qUnifiable state <*> (`S.notMember` sq_αs state)
fβlst ← case q1 of
-- (BOT-SAT)
Qu → return id
-- (BOT-UNSAT)
_ | S.null βs' → do
tErrExp_
[msg| Qualifier inequality unsatisfiable. |]
(pprMsg q1)
(pprMsg (QeU γs2))
return id
| otherwise →
return ((q1, βs') :)
let fvmap = M.unionWith mappend (setToMapWith bound γs')
bound γ
| M.lookup γ (sq_τftv state) == Just Covariant
, γ `S.member` sq_αs state
= qemSingleton maxBound
| qUnifiable state γ = qemSingleton (QeU γs2)
| otherwise = qemSingleton (QeU βs')
return state {
sq_βlst = fβlst (sq_βlst state),
sq_vmap = fvmap (sq_vmap state)
}
-- | Turn the decomposed constraint back into a list of pairs of types.
recomposeQuals ∷ Ord tv ⇒ QCState tv → [(Type tv, Type tv)]
recomposeQuals state =
[ (fvTy γ, clean βs)
| (γ, QEMeet qem) ← M.toList (sq_vmap state)
, γ `S.notMember` sq_αs state
, βs ← qem ]
++
[ (qualToType ql, clean βs)
| (ql, βs) ← sq_βlst state ]
where
clean βs = qualToType (βs S.\\ sq_αs state)
-- | Given a list of type variables and qualifiers, substitute for each,
-- updating the state as necessary.
qSubsts ∷ MonadConstraint tv r m ⇒
String → QCState tv → M.Map tv (QExp tv) → m (QCState tv)
qSubsts who state γqes0
| M.null γqes0 = return state
| otherwise = do
traceN 4 (who, γqes0, state)
let sanitize _ [] []
= typeBug "subst" $
"Attempted impossible substitution: " ++ show γqes0
sanitize _ acc []
= unsafeSubsts state (M.fromDistinctAscList (reverse acc))
sanitize seen acc ((γ, qe):rest)
| S.member γ (S.union seen (ftvSet qe))
= sanitize seen acc rest
| otherwise
= sanitize (seen `S.union` ftvSet qe) ((γ, qe):acc) rest
sanitize S.empty [] (M.toAscList γqes0)
where
--
-- This does the main work of substitution, and it has a funny
-- precondition (which is enforced by 'subst', above), namely:
-- the type variables will be substituted in increasing order, so the
-- image of later variables must not contain earlier variables.
--
-- This is okay: { 1 ↦ 2 3, 2 ↦ 4 }
-- This is not okay: { 1 ↦ 3 4, 2 ↦ 1 }
unsafeSubsts state γqes = do
sequence [ do
let τ = qualToType (liftVQExp qe)
writeTV γ τ
updatePinnedTVs γ τ
| (γ, qe) ← M.toList γqes ]
let γset = M.keysSet γqes
unchanged set = S.null (γset `S.intersection` set)
(βlst, βlst') = List.partition (unchanged . snd) (sq_βlst state)
(vmap, vmap') = M.partitionWithKey
(curry (unchanged . ftvSet))
(sq_vmap state)
let ineqs =
[ (qualToType ql, qualToType βs)
| (ql, βs) ← βlst' ]
++
[ (fvTy γ, qualToType qe)
| (γ, qem) ← M.toList vmap'
, qe ← unQEMeet qem ]
state ← decomposeQuals ineqs
state {
sq_αs = sq_αs state S.\\ γset,
sq_τftv = M.foldrWithKey substQE (sq_τftv state) γqes,
sq_βlst = βlst,
sq_vmap = vmap
}
traceN 4 ("subst", γqes, state)
return state
-- | Substitute and simplify a qualifier expression
simplifyQual ∷ (MonadSubst tv r m, Qualifier q tv) ⇒
q → m (QExp tv)
simplifyQual q = do
qe ← qualifier <$> subst (qualToType q)
case qe of
QeA → return QeA
QeU γs → do
(γs', qls) ← partitionJust tvQual <$> mapM fromTyVar (S.toAscList γs)
case bigJoin qls of
Qa → return QeA
_ → return (QeU (S.fromDistinctAscList γs'))
---
--- SAT SOLVING FOR QUALIFIER CONSTRAINTS
---
--
-- As a last ditch effort, use a simple SAT solver to find a
-- decent literal-only substitution.
runSat ∷ MonadConstraint tv r m ⇒
QCState tv → Bool → m (QCState tv)
runSat state doIt = do
let sols = SAT.solve =<< SAT.assertTrue formula SAT.newSatSolver
traceN 4 ("runSat", formula, sols)
case sols of
[] → do
typeError_ [msg| Qualifier constraints unsatisfiable |]
return state
sat:_ | doIt
→ qSubsts "sat" state =<<
M.fromDistinctAscList <$> sequence
[ return (δ, qlitexp ql)
-- warn $ "\nSAT: substituting " ++ show (QE ql slack) ++
-- " for type variable " ++ show δ
| δ ← S.toAscList (sq_αs state)
, qUnifiable state δ
, let (ql, var) = decodeSatVar δ (sq_τftv state) sat
, ql == Qa || var /= QInvariant ]
_ → return state
where
formula = foldr (SAT.:&&:) SAT.Yes $
[ (πa τftv q ==> πa τftv βs)
| (q, βs) ← sq_βlst state ]
++
[ (πa τftv (Free α) ==> πa τftv αs)
| (α, QEMeet qes) ← M.toList (sq_vmap state)
, qUnifiable state α
, αs ← qes ]
p ==> q = SAT.Not p SAT.:||: q
τftv = sq_τftv state
-- | To encode some qualifier as a SAT formula
class SATable a v where
πa ∷ VarMap v → a → SAT.Boolean
instance SATable QLit v where
πa _ Qa = SAT.Yes
πa _ _ = SAT.No
instance Tv v ⇒ SATable (TyVar v) v where
πa vm (Free β) = encodeSatVar β vm
πa _ _ = SAT.No
instance Tv v ⇒ SATable (S.Set v) v where
πa vm vs = S.fold ((SAT.:||:) . πa vm . Free) SAT.No vs
-- | Given a type variable and a SAT solution, return a bound
-- for that type variable as implied by the solution.
decodeSatVar ∷ Tv tv ⇒ tv → VarMap tv → SAT.SatSolver → (QLit, Variance)
decodeSatVar β vm solver = (q, var) where
(maximize, var) = maximizeVariance β vm
q = case (maximize, mba) of
-- For minimizing variables, each component tells us whether that
-- component may be omitted from the substitution, so we choose the
-- smallest qualifier literal that includes the required components.
(False, Just False) → Qa
(False, _ ) → Qu
-- For maximizing variables, each component tells us whether that
-- component may be included in the substitution, so we choose the
-- largest qualifier literal that omits the forbidden components.
(True , Just False) → Qu
(True , _ ) → Qa
mba = SAT.lookupVar βa solver
βa = tvUniqueID β
-- | Encode the 'q' component of type variable 'β'. We want to maximize
-- contravariant variables and minimize all the others. Since the
-- solver tries true before false, we use a positive literal to stand
-- for the 'q' component of a maximized variable and a negative
-- literal for a minimized variable.
encodeSatVar ∷ Tv tv ⇒ tv → VarMap tv → SAT.Boolean
encodeSatVar β vm
| fst (maximizeVariance β vm) = SAT.Var z
| otherwise = SAT.Not (SAT.Var z)
where z = tvUniqueID β
maximizeVariance ∷ Ord tv ⇒ tv → VarMap tv → (Bool, Variance)
maximizeVariance γ vm = case M.findWithDefault 0 γ vm of
v@QCovariant → (False, v)
v@QInvariant → (False, v)
v → (True, v)
instance Ppr.Ppr SAT.Boolean where pprPrec = Ppr.pprFromShow
instance Ppr.Ppr SAT.SatSolver where pprPrec = Ppr.pprFromShow
---
--- General qualifier-solving utility functions
---
-- | Is the given type variable unifiable as a qualifier variable?
-- Right now, this just means its kind is 'KdQual'.
qUnifiable ∷ Tv tv ⇒ QCState tv → tv → Bool
qUnifiable _ α = tvKindIs KdQual α
-- | Project a free type variable from a 'TyVar', or error if the
-- 'TyVar' is bounds.
fromTyVar ∷ MonadAlmsError m ⇒ TyVar tv → m tv
fromTyVar (Free α) = return α
fromTyVar _ = typeBug "solveQualifiers" "Got bound type variable"
-- | Update a type variable variance map as a result of substituting a
-- qualifier expression for a type variable.
substQE ∷ Ord tv ⇒ tv → QExp tv → VarMap tv → VarMap tv
substQE β qe vmap = case takeMap β vmap of
(Just v, vmap') → M.unionWith (⊔) vmap' (setToMap v (ftvSet qe))
_ → vmap
-- | Lookup a key in a map and remove the key from the map.
takeMap ∷ Ord k ⇒ k → M.Map k v → (Maybe v, M.Map k v)
takeMap = M.updateLookupWithKey (\_ _ → Nothing)
-- | Lift a 'S.Set' to a 'M.Map' with constant value
setToMap ∷ a → S.Set k → M.Map k a
setToMap = setToMapWith . const
-- | Lift a 'S.Set' to a 'M.Map' with values computed from keys.
setToMapWith ∷ (k → a) → S.Set k → M.Map k a
setToMapWith f = M.fromDistinctAscList . map (id &&& f) . S.toAscList
{-
OPTIMIZATIONS FROM SIMONET 2003
6.1 Collapsing Cycles
This is the SCC phase
6.2 Polarities (implemented in buildGraph)
Upper bounds on positive variables and lower bounds on negative
variables are irrelevant, e.g.:
f : ∀ α ≤ A. 1 → α × α
f : ∀ α. 1 → α × α
Or:
let rec f = λx. f (f x) in f
f : α → β [β ≤ α]
f : ∀α. ∀β ≤ α. α → β
f : ∀α. ∀β. α → β
6.3 Reducing Chains (implemented in polarizedReduce)
A positive variable with a single predecessor can be fused with the
predecessor; dually, a negative variable can be fused with a single
successor.
∀ α ≤ A. α → 1
A → 1
∀ α ≤ A. α × α → 1
A × A → 1
Currently this is implemented only for variables that occur only once.
Why?
6.4 Polarized Garbage Collection
?
6.5 Minimization
If two positive variables have all the same predecessors, the can be
coalesced. Dually for negative variables with the same successors.
∀ α ≤ C. ∀ β ≤ C. α × β → 1
A × B → 1
∀ α ≤ C. α × α → 1
C × C → 1
A × B → 1
-}