{-# 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(..))
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 :: CtLoc -> PredType -> EvTerm -> TcPluginM CtEvidence
newGiven :: CtLoc -> PredType -> EvTerm -> TcPluginM CtEvidence
newGiven CtLoc
loc PredType
pty (EvExpr EvExpr
ev) = CtLoc -> PredType -> EvExpr -> TcPluginM CtEvidence
TcPlugin.newGiven CtLoc
loc PredType
pty EvExpr
ev
newGiven CtLoc
_ PredType
_  EvTerm
ev = forall a. String -> SDoc -> a
panicDoc String
"newGiven: not an EvExpr: " (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
_)]
    = forall a. a -> Maybe a
Just
    forall a b. (a -> b) -> a -> b
$ CtEvidence -> Ct
mkNonCanonical
    forall a b. (a -> b) -> a -> b
$ PredType -> TcTyVar -> CtLoc -> CtEvidence
CtGiven (PredType -> PredType -> PredType
mkPrimEqPred PredType
lhs PredType
rhs)
              (Ct -> TcTyVar
ctEvId Ct
ct)
              (Ct -> CtLoc
ctLoc Ct
ct)

flatToCt [((TcTyVar, PredType), 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 {CtEvidence
CanEqLHS
EqRel
PredType
cc_eq_rel :: Ct -> EqRel
cc_ev :: Ct -> CtEvidence
cc_lhs :: Ct -> CanEqLHS
cc_rhs :: Ct -> PredType
cc_eq_rel :: EqRel
cc_rhs :: PredType
cc_lhs :: CanEqLHS
cc_ev :: CtEvidence
..})
  | TyVarLHS TcTyVar
tyvar <- CanEqLHS
cc_lhs
  = forall a. a -> Maybe a
Just ((TcTyVar
tyvar,PredType
cc_rhs),Ct
ct)
mkSubst 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 :: CtEvidence
qci_ev = CtEvidence
ev { ctev_pred :: PredType
ctev_pred = PredType -> PredType
f (CtEvidence -> PredType
ctev_pred CtEvidence
ev) } } )
overEvidencePredType PredType -> PredType
f Ct
ct =
  let
    ev :: CtEvidence
    ev :: CtEvidence
ev = Ct -> CtEvidence
cc_ev Ct
ct
  in Ct
ct { cc_ev :: CtEvidence
cc_ev = CtEvidence
ev { ctev_pred :: PredType
ctev_pred = PredType -> PredType
f (CtEvidence -> PredType
ctev_pred CtEvidence
ev) } }