Unification.hs

{-# LANGUAGE CPP #-}

module Polysemy.Plugin.Fundep.Unification where

import           Data.Bool
import           Data.Function (on)
import           Data.Set (Set)
import qualified Data.Set as S

#if __GLASGOW_HASKELL__ >= 900
import           GHC.Tc.Types.Constraint
#elif __GLASGOW_HASKELL__ >= 810
import           Constraint
#else
import           TcRnTypes
#endif

#if __GLASGOW_HASKELL__ >= 900
import           GHC.Core.Type
import           GHC.Core.Unify
import           GHC.Plugins (Outputable, ppr, parens, text, (<+>))
#else
import           Type
import           Unify
import           GhcPlugins (Outputable, ppr, parens, text, (<+>))
#endif

#if __GLASGOW_HASKELL__ >= 906
#define SUBST Subst
import           GHC.Core.TyCo.Subst (SUBST)
import           GHC.Core.TyCo.Compare (eqType, nonDetCmpType)
#else
#define SUBST TCvSubst
#endif


------------------------------------------------------------------------------
-- | The context in which we're attempting to solve a constraint.
data SolveContext
  = -- | In the context of a function definition. The @Set TyVar@ is all of the
    -- skolems that exist in the [G] constraints for this function.
    FunctionDef (Set TyVar)
    -- | In the context of running an interpreter. The 'Bool' corresponds to
    -- whether we are only trying to solve a single 'Member' constraint right
    -- now. If so, we *must* produce a unification wanted.
  | InterpreterUse Bool (Set TyVar)
  deriving (Eq, Ord)

instance Outputable SolveContext where
  ppr (FunctionDef s) = parens $ text "FunctionDef" <+> ppr s
  ppr (InterpreterUse s ty) = parens $ text "InterpreterUse" <+> ppr s <+> ppr ty


------------------------------------------------------------------------------
-- | Depending on the context in which we're solving a constraint, we may or
-- may not want to force a unification of effects. For example, when defining
-- user code whose type is @Member (State Int) r => ...@, if we see @get :: Sem
-- r s@, we should unify @s ~ Int@.
mustUnify :: SolveContext -> Bool
mustUnify (FunctionDef _) = True
mustUnify (InterpreterUse b _) = b


------------------------------------------------------------------------------
-- | Determine whether or not two effects are unifiable.
--
-- All free variables in [W] constraints are considered skolems, and thus are
-- not allowed to unify with anything but themselves. This properly handles all
-- cases in which we are unifying ambiguous [W] constraints (which are true
-- type variables) against [G] constraints.
unify
    :: SolveContext
    -> Type  -- ^ wanted
    -> Type  -- ^ given
    -> Maybe SUBST
unify solve_ctx = tryUnifyUnivarsButNotSkolems skolems
  where
    skolems :: Set TyVar
    skolems =
      case solve_ctx of
        InterpreterUse _ s -> s
        FunctionDef s      -> s

#if __GLASGOW_HASKELL__ >= 902
#define BINDME (const BindMe)
#define APART (const Apart)
#else
#define BINDME BindMe
#define APART Skolem
#endif

tryUnifyUnivarsButNotSkolems :: Set TyVar -> Type -> Type -> Maybe SUBST
tryUnifyUnivarsButNotSkolems skolems goal inst =
  case tcUnifyTysFG
         (bool BINDME APART . flip S.member skolems)
         [inst]
         [goal] of
    Unifiable subst -> pure subst
    _               -> Nothing

------------------------------------------------------------------------------
-- | A wrapper for two types that we want to say have been unified.
data Unification = Unification
  { _unifyLHS :: OrdType
  , _unifyRHS :: OrdType
  }
  deriving (Eq, Ord)


------------------------------------------------------------------------------
-- | 'Type's don't have 'Eq' or 'Ord' instances by default, even though there
-- are functions in GHC that implement these operations. This newtype gives us
-- those instances.
newtype OrdType = OrdType
  { getOrdType :: Type
  }

instance Eq OrdType where
  (==) = eqType `on` getOrdType

instance Ord OrdType where
  compare = nonDetCmpType `on` getOrdType


------------------------------------------------------------------------------
-- | Filter out the unifications we've already emitted, and then give back the
-- things we should put into the @S.Set Unification@, and the new constraints
-- we should emit.
unzipNewWanteds
    :: S.Set Unification
    -> [(Unification, Ct)]
    -> ([Unification], [Ct])
unzipNewWanteds old = unzip . filter (not . flip S.member old . fst)