{-# LANGUAGE RecordWildCards #-}

module Internal.Constraint (newGiven, flatToCt, mkSubst, overEvidencePredType) where

import GhcApi.GhcPlugins
import GhcApi.Constraint
  (Ct(..), CtEvidence(..), CanEqLHS(..), CtLoc, ctLoc, ctEvId, mkNonCanonical)

import GHC.Tc.Utils.TcType (TcType)
import GHC.Tc.Types.Constraint (QCInst(..))
import GHC.Tc.Types.Evidence (EvTerm(..), EvBindsVar)
import GHC.Tc.Plugin (TcPluginM)
import qualified GHC.Tc.Plugin as TcPlugin (newGiven)

-- | Create a new [G]iven constraint, with the supplied evidence. This must not
-- be invoked from 'tcPluginInit' or 'tcPluginStop', or it will panic.
newGiven :: EvBindsVar -> CtLoc -> PredType -> EvTerm -> TcPluginM CtEvidence
newGiven :: EvBindsVar -> CtLoc -> PredType -> EvTerm -> TcPluginM CtEvidence
newGiven EvBindsVar
tcEvbinds CtLoc
loc PredType
pty (EvExpr EvExpr
ev) = EvBindsVar -> CtLoc -> PredType -> EvExpr -> TcPluginM CtEvidence
TcPlugin.newGiven EvBindsVar
tcEvbinds CtLoc
loc PredType
pty EvExpr
ev
newGiven EvBindsVar
_ CtLoc
_ PredType
_ EvTerm
ev = String -> SDoc -> TcPluginM CtEvidence
forall a. String -> SDoc -> a
panicDoc String
"newGiven: not an EvExpr: " (EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
ev)

flatToCt :: [((TcTyVar,TcType),Ct)] -> Maybe Ct
flatToCt :: [((TcTyVar, PredType), Ct)] -> Maybe Ct
flatToCt [((TcTyVar
_,PredType
lhs),Ct
ct),((TcTyVar
_,PredType
rhs),Ct
_)]
    = Ct -> Maybe Ct
forall a. a -> Maybe a
Just
    (Ct -> Maybe Ct) -> Ct -> Maybe Ct
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Ct
mkNonCanonical
    (CtEvidence -> Ct) -> CtEvidence -> Ct
forall a b. (a -> b) -> a -> b
$ PredType -> TcTyVar -> CtLoc -> CtEvidence
CtGiven (PredType -> PredType -> PredType
mkPrimEqPred PredType
lhs PredType
rhs)
              ((() :: Constraint) => Ct -> TcTyVar
Ct -> TcTyVar
ctEvId Ct
ct)
              (Ct -> CtLoc
ctLoc Ct
ct)

flatToCt [((TcTyVar, PredType), Ct)]
_ = Maybe Ct
forall a. Maybe a
Nothing

-- | Create simple substitution from type equalities
mkSubst :: Ct -> Maybe ((TcTyVar, TcType),Ct)
mkSubst :: Ct -> Maybe ((TcTyVar, PredType), Ct)
mkSubst ct :: Ct
ct@(CEqCan {PredType
EqRel
CtEvidence
CanEqLHS
cc_ev :: CtEvidence
cc_lhs :: CanEqLHS
cc_rhs :: PredType
cc_eq_rel :: EqRel
cc_ev :: Ct -> CtEvidence
cc_lhs :: Ct -> CanEqLHS
cc_rhs :: Ct -> PredType
cc_eq_rel :: Ct -> EqRel
..})
  | TyVarLHS TcTyVar
tyvar <- CanEqLHS
cc_lhs
  = ((TcTyVar, PredType), Ct) -> Maybe ((TcTyVar, PredType), Ct)
forall a. a -> Maybe a
Just ((TcTyVar
tyvar,PredType
cc_rhs),Ct
ct)
mkSubst Ct
_ = Maybe ((TcTyVar, PredType), Ct)
forall a. Maybe a
Nothing

-- | Modify the predicate type of the evidence term of a constraint
overEvidencePredType :: (TcType -> TcType) -> Ct -> Ct
overEvidencePredType :: (PredType -> PredType) -> Ct -> Ct
overEvidencePredType PredType -> PredType
f (CQuantCan QCInst
qci) =
  let
    ev :: CtEvidence
    ev :: CtEvidence
ev = QCInst -> CtEvidence
qci_ev QCInst
qci
  in QCInst -> Ct
CQuantCan ( QCInst
qci { qci_ev = ev { ctev_pred = f (ctev_pred ev) } } )
overEvidencePredType PredType -> PredType
f Ct
ct =
  let
    ev :: CtEvidence
    ev :: CtEvidence
ev = Ct -> CtEvidence
cc_ev Ct
ct
  in Ct
ct { cc_ev = ev { ctev_pred = f (ctev_pred ev) } }