-
Notifications
You must be signed in to change notification settings - Fork 9
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
702dda2
commit 7839d31
Showing
9 changed files
with
161 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
module GhcApi.Constraint | ||
( Ct(..) | ||
, CtEvidence(..) | ||
, CtLoc | ||
, CanEqLHS(..) | ||
, ctLoc | ||
, ctEvId | ||
, mkNonCanonical | ||
) | ||
where | ||
|
||
import GHC.Tc.Types.Constraint | ||
(Ct (..), CtEvidence (..), CanEqLHS (..), CtLoc, ctLoc, ctEvId, mkNonCanonical) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
module GhcApi.GhcPlugins (module GHC.Plugins, FindResult(..), findPluginModule) where | ||
|
||
import GHC.Plugins hiding (TcPlugin) | ||
import GHC.Unit.Finder (findPluginModule) | ||
import GHC.Tc.Plugin (FindResult(..)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,64 @@ | ||
{-# 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 (DictCt(..), IrredCt(..), EqCt(..), 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 tcEvbinds loc pty (EvExpr ev) = TcPlugin.newGiven tcEvbinds loc pty ev | ||
newGiven _ _ _ ev = panicDoc "newGiven: not an EvExpr: " (ppr ev) | ||
|
||
flatToCt :: [((TcTyVar,TcType),Ct)] -> Maybe Ct | ||
flatToCt [((_,lhs),ct),((_,rhs),_)] | ||
= Just | ||
$ mkNonCanonical | ||
$ CtGiven (mkPrimEqPred lhs rhs) | ||
(ctEvId ct) | ||
(ctLoc ct) | ||
|
||
flatToCt _ = Nothing | ||
|
||
-- | Create simple substitution from type equalities | ||
mkSubst :: Ct -> Maybe ((TcTyVar, TcType),Ct) | ||
mkSubst ct@(CEqCan (EqCt {..})) | ||
| TyVarLHS tyvar <- eq_lhs | ||
= Just ((tyvar,eq_rhs),ct) | ||
mkSubst _ = Nothing | ||
|
||
-- | Modify the predicate type of the evidence term of a constraint | ||
overEvidencePredType :: (TcType -> TcType) -> Ct -> Ct | ||
overEvidencePredType f (CDictCan di) = | ||
let | ||
ev :: CtEvidence | ||
ev = di_ev di | ||
in CDictCan ( di { di_ev = ev { ctev_pred = f (ctev_pred ev) } } ) | ||
overEvidencePredType f (CIrredCan ir) = | ||
let | ||
ev :: CtEvidence | ||
ev = ir_ev ir | ||
in CIrredCan ( ir { ir_ev = ev { ctev_pred = f (ctev_pred ev) } } ) | ||
overEvidencePredType f (CEqCan eq) = | ||
let | ||
ev :: CtEvidence | ||
ev = eq_ev eq | ||
in CEqCan ( eq { eq_ev = ev { ctev_pred = f (ctev_pred ev) } } ) | ||
overEvidencePredType f (CNonCanonical ct) = | ||
let | ||
ev :: CtEvidence | ||
ev = ct | ||
in CNonCanonical ( ev { ctev_pred = f (ctev_pred ev) } ) | ||
overEvidencePredType f (CQuantCan qci) = | ||
let | ||
ev :: CtEvidence | ||
ev = qci_ev qci | ||
in CQuantCan ( qci { qci_ev = ev { ctev_pred = f (ctev_pred ev) } } ) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
module Internal.Evidence (evByFiat, evByFiatWithDependencies) where | ||
|
||
import GHC.Tc.Types.Evidence (EvTerm(..)) | ||
import GHC.Core.TyCo.Rep (UnivCoProvenance (..)) | ||
|
||
import GhcApi.GhcPlugins | ||
|
||
-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce' | ||
evByFiat :: String -- ^ Name the coercion should have | ||
-> Type -- ^ The LHS of the equivalence relation (~) | ||
-> Type -- ^ The RHS of the equivalence relation (~) | ||
-> EvTerm | ||
evByFiat name t1 t2 = | ||
EvExpr $ Coercion $ mkUnivCo (PluginProv name emptyDVarSet) Nominal t1 t2 | ||
{-# DEPRECATED evByFiat "'evByFiat' creates proofs that can lead to unsoundness, use 'evByFiatWithDependencies' instead.\nSee also https://gitlab.haskell.org/ghc/ghc/-/merge_requests/12037" #-} | ||
|
||
-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce' | ||
evByFiatWithDependencies :: | ||
String -- ^ Name the coercion should have | ||
-> DCoVarSet -- ^ The set of all the in-scope coercion variables | ||
-- that the proof makes use of. | ||
-> Type -- ^ The LHS of the equivalence relation (~) | ||
-> Type -- ^ The RHS of the equivalence relation (~) | ||
-> EvTerm | ||
evByFiatWithDependencies name deps t1 t2 = | ||
EvExpr $ Coercion $ mkUnivCo (PluginProv name deps) Nominal t1 t2 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,30 @@ | ||
module Internal.Type (substType) where | ||
|
||
import Data.Maybe (fromMaybe) | ||
import GHC.Tc.Utils.TcType (TcType) | ||
import GHC.Core.TyCo.Rep (Type (..)) | ||
import GHC.Types.Var (TcTyVar) | ||
|
||
-- | Apply substitutions in Types | ||
-- | ||
-- __NB:__ Doesn't substitute under binders | ||
substType | ||
:: [(TcTyVar, TcType)] | ||
-> TcType | ||
-> TcType | ||
substType subst tv@(TyVarTy v) = | ||
fromMaybe tv (lookup v subst) | ||
substType subst (AppTy t1 t2) = | ||
AppTy (substType subst t1) (substType subst t2) | ||
substType subst (TyConApp tc xs) = | ||
TyConApp tc (map (substType subst) xs) | ||
substType _subst t@(ForAllTy _tv _ty) = | ||
-- TODO: Is it safe to do "dumb" substitution under binders? | ||
-- ForAllTy tv (substType subst ty) | ||
t | ||
substType subst (FunTy k1 k2 t1 t2) = | ||
FunTy k1 k2 (substType subst t1) (substType subst t2) | ||
substType _ l@(LitTy _) = l | ||
substType subst (CastTy ty co) = | ||
CastTy (substType subst ty) co | ||
substType _ co@(CoercionTy _) = co |