diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,29 @@ +## 0.5 *March 4th 2024* +* Add `evByFiatWithDependencies`, see https://gitlab.haskell.org/ghc/ghc/-/merge_requests/12037 for more details. +* Added support for GHC 9.12.1 + +## 0.4.6 *May 22nd 2024* +* Added support for GHC-9.10.1 +* Removed support for GHC 7.10 + +## 0.4.5 *October 10th 2023* +* Support for GHC-9.8.1 + +## 0.4.4 *February 20th 2023* +* Support for GHC-9.6.0.20230210 + +## 0.4.3 *September 2nd 2022* +* Support for GHC-9.4.2 + +## 0.4.2 *June 17th 2021* +* Support for GHC-9.2.0.20210422 + +## 0.4.1 *January 1st 2021* +* Support for GHC-9.0.1-rc1 + +## 0.4 *January 31st 2020* +* Expose functions for flattening constraints in GHC 8.2 and earlier + ## 0.3.2 *January 18th 2020* * [#11](https://github.com/clash-lang/ghc-tcplugins-extra/pull/11) Support `-hide-all-plugin-packages`/`-plugin-package-id` diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,6 +1,7 @@ # ghc-tcplugins-extra Utilities for writing GHC type-checker plugins -[![Build Status](https://secure.travis-ci.org/clash-lang/ghc-tcplugins-extra.svg?branch=master)](http://travis-ci.org/clash-lang/ghc-tcplugins-extra) +[![Build Status (cabal)](https://github.com/clash-lang/ghc-tcplugins-extra/actions/workflows/haskell-ci.yml/badge.svg)](https://github.com/clash-lang/ghc-tcplugins-extra-undef/actions/workflows/haskell-ci.yml) +[![Build Status (stack)](https://github.com/clash-lang/ghc-tcplugins-extra/actions/workflows/stack.yml/badge.svg)](https://github.com/clash-lang/ghc-tcplugins-extra-undef/actions/workflows/stack.yml) [![Hackage](https://img.shields.io/hackage/v/ghc-tcplugins-extra.svg)](https://hackage.haskell.org/package/ghc-tcplugins-extra) [![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-tcplugins-extra.svg?style=flat)](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-tcplugins-extra) diff --git a/defaults.dhall b/defaults.dhall new file mode 100644 --- /dev/null +++ b/defaults.dhall @@ -0,0 +1,44 @@ +{ name = "ghc-tcplugins-extra" +, version = "0.5" +, synopsis = "Utilities for writing GHC type-checker plugins" +, description = + '' + Utilities for writing GHC type-checker plugins, such as + creating constraints, with a stable API covering multiple + GHC releases.'' +, category = "Type System" +, author = "Christiaan Baaij" +, maintainer = "christiaan.baaij@gmail.com" +, copyright = + '' + Copyright © 2015-2016, University of Twente, + 2017-2018, QBayLogic'' +, github = "clash-lang/ghc-tcplugins-extra" +, license = "BSD2" +, license-file = "LICENSE" +, tested-with = + "GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5, GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8, GHC == 9.4.7, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.1, GHC == 9.12.1" +, extra-source-files = + [ "README.md", "CHANGELOG.md", "defaults.dhall", "package.dhall" ] +, ghc-options = [ "-Wall" ] +, flags.deverror + = + { description = "Enables `-Werror` for development mode and TravisCI" + , default = False + , manual = True + } +, when = + [ { condition = "impl(ghc >= 8.0.0)" + , ghc-options = + [ "-Wcompat" + , "-Wincomplete-uni-patterns" + , "-Widentities" + , "-Wredundant-constraints" + ] + } + , { condition = "impl(ghc >= 8.4.0)" + , ghc-options = [ "-fhide-source-paths" ] + } + , { condition = "flag(deverror)", ghc-options = [ "-Werror" ] } + ] +} diff --git a/ghc-tcplugins-extra.cabal b/ghc-tcplugins-extra.cabal --- a/ghc-tcplugins-extra.cabal +++ b/ghc-tcplugins-extra.cabal @@ -1,46 +1,233 @@ -name: ghc-tcplugins-extra -version: 0.3.2 -synopsis: Utilities for writing GHC type-checker plugins -description: Utilities for writing GHC type-checker plugins, such as - creating constraints, with a stable API covering multiple - GHC releases. -homepage: http://github.com/clash-lang/ghc-tcplugins-extra -bug-reports: http://github.com/clash-lang/ghc-tcplugins-extra/issues -license: BSD2 -license-file: LICENSE -author: Christiaan Baaij -maintainer: christiaan.baaij@gmail.com -copyright: Copyright © 2015-2016, University of Twente, - 2017-2018, QBayLogic -category: Type System -build-type: Simple -extra-source-files: README.md - CHANGELOG.md -cabal-version: >=1.10 -tested-with: GHC == 7.10.3, GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, - GHC == 8.6.5, GHC == 8.8.2, GHC == 8.10.1 +cabal-version: 2.0 +-- This file has been generated from package.dhall by hpack version 0.35.5. +-- +-- see: https://github.com/sol/hpack + +name: ghc-tcplugins-extra +version: 0.5 +synopsis: Utilities for writing GHC type-checker plugins +description: Utilities for writing GHC type-checker plugins, such as + creating constraints, with a stable API covering multiple + GHC releases. +category: Type System +homepage: https://github.com/clash-lang/ghc-tcplugins-extra#readme +bug-reports: https://github.com/clash-lang/ghc-tcplugins-extra/issues +author: Christiaan Baaij +maintainer: christiaan.baaij@gmail.com +copyright: Copyright © 2015-2016, University of Twente, + 2017-2018, QBayLogic +license: BSD2 +license-file: LICENSE +build-type: Simple +tested-with: + GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5, GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8, GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.1, GHC == 9.12.1 +extra-source-files: + README.md + CHANGELOG.md + defaults.dhall + package.dhall + source-repository head type: git - location: https://github.com/clash-lang/ghc-tcplugins-extra.git + location: https://github.com/clash-lang/ghc-tcplugins-extra flag deverror - description: - Enables `-Werror` for development mode and TravisCI - default: False + description: Enables `-Werror` for development mode and TravisCI manual: True + default: False library - exposed-modules: GHC.TcPluginM.Extra - build-depends: base >=4.8 && <5, - ghc >=7.10 && <8.12 - hs-source-dirs: src - default-language: Haskell2010 - other-extensions: CPP - LambdaCase - RecordWildCards - PatternSynonyms + exposed-modules: + GHC.TcPluginM.Extra + other-modules: + Internal + hs-source-dirs: + src + ghc-options: -Wall + build-depends: + base >=4.8 && <5 + , ghc >=7.10 && <9.13 + default-language: Haskell2010 + if impl(ghc >= 8.0.0) + ghc-options: -Wcompat -Wincomplete-uni-patterns -Widentities -Wredundant-constraints + if impl(ghc >= 8.4.0) + ghc-options: -fhide-source-paths if flag(deverror) - ghc-options: -Wall -Werror - else - ghc-options: -Wall + ghc-options: -Werror + if impl(ghc >= 9.11) && impl(ghc < 9.13) + other-modules: + GhcApi.Constraint + GhcApi.Predicate + GhcApi.GhcPlugins + Internal.Type + Internal.Constraint + Internal.Evidence + hs-source-dirs: + src-ghc-tree-9.4 + src-ghc-9.12 + build-depends: + ghc >=9.11 && <9.13 + if impl(ghc >= 9.10) && impl(ghc < 9.11) + other-modules: + GhcApi.Constraint + GhcApi.Predicate + GhcApi.GhcPlugins + Internal.Type + Internal.Constraint + Internal.Evidence + hs-source-dirs: + src-ghc-tree-9.4 + src-ghc-9.10 + build-depends: + ghc ==9.10.* + if impl(ghc >= 9.8) && impl(ghc < 9.10) + other-modules: + GhcApi.Constraint + GhcApi.Predicate + GhcApi.GhcPlugins + Internal.Type + Internal.Constraint + Internal.Evidence + hs-source-dirs: + src-ghc-tree-9.4 + src-ghc-9.8 + build-depends: + ghc >=9.8 && <9.10 + if impl(ghc >= 9.4) && impl(ghc < 9.8) + other-modules: + GhcApi.Constraint + GhcApi.Predicate + GhcApi.GhcPlugins + Internal.Type + Internal.Constraint + Internal.Evidence + hs-source-dirs: + src-ghc-tree-9.4 + src-ghc-9.4 + build-depends: + ghc >=9.4 && <9.8 + if impl(ghc >= 9.2) && impl(ghc < 9.4) + other-modules: + GhcApi.Constraint + GhcApi.Predicate + GhcApi.GhcPlugins + Internal.Type + Internal.Constraint + Internal.Evidence + hs-source-dirs: + src-ghc-tree + src-ghc-9.2 + build-depends: + ghc >=9.2 && <9.4 + if impl(ghc >= 9.0) && impl(ghc < 9.2) + other-modules: + GhcApi.Constraint + GhcApi.Predicate + GhcApi.GhcPlugins + Internal.Type + Internal.Constraint + Internal.Evidence + hs-source-dirs: + src-ghc-tree + src-ghc-9.0 + build-depends: + ghc >=9.0 && <9.2 + if impl(ghc >= 8.10) && impl(ghc < 9.0) + other-modules: + GhcApi.Constraint + GhcApi.Predicate + GhcApi.GhcPlugins + Internal.Type + Internal.Constraint + Internal.Evidence + hs-source-dirs: + src-ghc-flat + src-ghc-8.10 + build-depends: + ghc >=8.10 && <9.0 + if impl(ghc >= 8.8) && impl(ghc < 8.10) + other-modules: + GhcApi.Constraint + GhcApi.Predicate + GhcApi.GhcPlugins + Internal.Type + Internal.Constraint + Internal.Evidence + hs-source-dirs: + src-ghc-flat + src-ghc-8.8 + build-depends: + ghc >=8.8 && <8.10 + mixins: + ghc hiding () + , ghc (TcRnTypes as Constraint) + , ghc (Type as Predicate) + if impl(ghc >= 8.6) && impl(ghc < 8.8) + other-modules: + GhcApi.Constraint + GhcApi.Predicate + GhcApi.GhcPlugins + Internal.Type + Internal.Constraint + Internal.Evidence + hs-source-dirs: + src-ghc-flat + src-ghc-8.6 + build-depends: + ghc >=8.6 && <8.8 + mixins: + ghc hiding () + , ghc (TcRnTypes as Constraint) + , ghc (Type as Predicate) + if impl(ghc >= 8.4) && impl(ghc < 8.6) + other-modules: + GhcApi.Constraint + GhcApi.Predicate + GhcApi.GhcPlugins + Internal.Type + Internal.Constraint + Internal.Evidence + hs-source-dirs: + src-ghc-flat + src-ghc-8.4 + build-depends: + ghc >=8.4 && <8.6 + mixins: + ghc hiding () + , ghc (TcRnTypes as Constraint) + , ghc (Type as Predicate) + if impl(ghc >= 8.2) && impl(ghc < 8.4) + other-modules: + GhcApi.Constraint + GhcApi.Predicate + GhcApi.GhcPlugins + Internal.Type + Internal.Constraint + Internal.Evidence + hs-source-dirs: + src-ghc-flat + src-ghc-8.2 + build-depends: + ghc >=8.2 && <8.4 + mixins: + ghc hiding () + , ghc (TcRnTypes as Constraint) + , ghc (Type as Predicate) + if impl(ghc >= 8.0) && impl(ghc < 8.2) + other-modules: + GhcApi.Constraint + GhcApi.Predicate + GhcApi.GhcPlugins + Internal.Type + Internal.Constraint + Internal.Evidence + hs-source-dirs: + src-ghc-flat + src-ghc-8.0 + build-depends: + ghc >=8.0 && <8.2 + mixins: + ghc hiding () + , ghc (TcRnTypes as Constraint) + , ghc (Type as Predicate) diff --git a/package.dhall b/package.dhall new file mode 100644 --- /dev/null +++ b/package.dhall @@ -0,0 +1,47 @@ +let defs = ./defaults.dhall + +let version = ./version.dhall + +in let ghc = { name = "ghc", mixin = [] : List Text } + + in let gin = + ghc + // { mixin = + [ "hiding ()" + , "(TcRnTypes as Constraint)" + , "(Type as Predicate)" + ] + } + + in let mods = + [ "GhcApi.Constraint" + , "GhcApi.Predicate" + , "GhcApi.GhcPlugins" + , "Internal.Type" + , "Internal.Constraint" + , "Internal.Evidence" + ] + + in defs + // { library = + { source-dirs = "src" + , dependencies = + [ "base >=4.8 && <5", "ghc >=7.10 && <9.13" ] + , exposed-modules = "GHC.TcPluginM.Extra" + , other-modules = "Internal" + , when = + [ version "9.11" "9.13" [ "tree-9.4", "9.12" ] ghc mods + , version "9.10" "9.11" [ "tree-9.4", "9.10" ] ghc mods + , version "9.8" "9.10" [ "tree-9.4", "9.8" ] ghc mods + , version "9.4" "9.8" [ "tree-9.4", "9.4" ] ghc mods + , version "9.2" "9.4" [ "tree", "9.2" ] ghc mods + , version "9.0" "9.2" [ "tree", "9.0" ] ghc mods + , version "8.10" "9.0" [ "flat", "8.10" ] ghc mods + , version "8.8" "8.10" [ "flat", "8.8" ] gin mods + , version "8.6" "8.8" [ "flat", "8.6" ] gin mods + , version "8.4" "8.6" [ "flat", "8.4" ] gin mods + , version "8.2" "8.4" [ "flat", "8.2" ] gin mods + , version "8.0" "8.2" [ "flat", "8.0" ] gin mods + ] + } + } diff --git a/src-ghc-8.0/GhcApi/GhcPlugins.hs b/src-ghc-8.0/GhcApi/GhcPlugins.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.0/GhcApi/GhcPlugins.hs @@ -0,0 +1,5 @@ +module GhcApi.GhcPlugins (module GhcPlugins, TcTyVar, EvTerm(..)) where + +import GhcPlugins hiding (mkSubst) +import TcType (TcTyVar) +import TcEvidence (EvTerm(..)) diff --git a/src-ghc-8.0/Internal/Constraint.hs b/src-ghc-8.0/Internal/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.0/Internal/Constraint.hs @@ -0,0 +1,26 @@ +module Internal.Constraint (module TcPluginM, flatToCt, overEvidencePredType) where + +import GhcApi.GhcPlugins +import GhcApi.Constraint + (Ct(..), CtEvidence(..), ctLoc, ctEvId, mkNonCanonical) + +import TcType (TcType) +import TcPluginM (newGiven) + +flatToCt :: [((TcTyVar,TcType),Ct)] -> Maybe Ct +flatToCt [((_,lhs),ct),((_,rhs),_)] + = Just + $ mkNonCanonical + $ CtGiven (mkPrimEqPred lhs rhs) + (ctEvId (cc_ev ct)) + (ctLoc ct) + +flatToCt _ = Nothing + +-- | Modify the predicate type of the evidence term of a constraint +overEvidencePredType :: (TcType -> TcType) -> Ct -> Ct +overEvidencePredType f ct = + let + ev :: CtEvidence + ev = cc_ev ct + in ct { cc_ev = ev { ctev_pred = f (ctev_pred ev) } } diff --git a/src-ghc-8.0/Internal/Evidence.hs b/src-ghc-8.0/Internal/Evidence.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.0/Internal/Evidence.hs @@ -0,0 +1,24 @@ +module Internal.Evidence (evByFiat, evByFiatWithDependencies) where + +import TcEvidence (EvTerm(..)) +import TyCoRep (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 = + EvCoercion $ mkUnivCo (PluginProv name) Nominal t1 t2 + +-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce' +evByFiatWithDependencies :: + String -- ^ Name the coercion should have + -> [Coercion] -- ^ The set of all the in-scope coercion 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 = + EvCoercion $ mkUnivCo (PluginProv name) Nominal t1 t2 diff --git a/src-ghc-8.0/Internal/Type.hs b/src-ghc-8.0/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.0/Internal/Type.hs @@ -0,0 +1,27 @@ +module Internal.Type (substType) where + +import Data.Maybe (fromMaybe) +import TcType (TcTyVar, TcType) +import TyCoRep (Type (..)) + +-- | 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 _ l@(LitTy _) = l +substType subst (CastTy ty co) = + CastTy (substType subst ty) co +substType _ co@(CoercionTy _) = co diff --git a/src-ghc-8.10/GhcApi/GhcPlugins.hs b/src-ghc-8.10/GhcApi/GhcPlugins.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.10/GhcApi/GhcPlugins.hs @@ -0,0 +1,3 @@ +module GhcApi.GhcPlugins (module GhcPlugins) where + +import GhcPlugins hiding (TcPlugin, mkSubst) diff --git a/src-ghc-8.10/Internal/Constraint.hs b/src-ghc-8.10/Internal/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.10/Internal/Constraint.hs @@ -0,0 +1,41 @@ +module Internal.Constraint (newGiven, flatToCt, overEvidencePredType) where + +import GhcApi.GhcPlugins +import GhcApi.Constraint + (Ct(..), CtEvidence(..), CtLoc, ctLoc, ctEvId, mkNonCanonical) + +import Panic (panicDoc) +import TcType (TcType) +import Constraint (QCInst(..)) +import TcEvidence (EvTerm(..)) +import TcPluginM (TcPluginM) +import qualified TcPluginM (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 loc pty (EvExpr ev) = TcPluginM.newGiven 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 + +-- | Modify the predicate type of the evidence term of a constraint +overEvidencePredType :: (TcType -> TcType) -> Ct -> Ct +overEvidencePredType f (CQuantCan qci) = + let + ev :: CtEvidence + ev = qci_ev qci + in CQuantCan ( qci { qci_ev = ev { ctev_pred = f (ctev_pred ev) } } ) +overEvidencePredType f ct = + let + ev :: CtEvidence + ev = cc_ev ct + in ct { cc_ev = ev { ctev_pred = f (ctev_pred ev) } } diff --git a/src-ghc-8.10/Internal/Evidence.hs b/src-ghc-8.10/Internal/Evidence.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.10/Internal/Evidence.hs @@ -0,0 +1,24 @@ +module Internal.Evidence (evByFiat, evByFiatWithDependencies) where + +import TcEvidence (EvTerm(..)) +import TyCoRep (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) Nominal t1 t2 + +-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce' +evByFiatWithDependencies :: + String -- ^ Name the coercion should have + -> [Coercion] -- ^ The set of all the in-scope coercion 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) Nominal t1 t2 diff --git a/src-ghc-8.10/Internal/Type.hs b/src-ghc-8.10/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.10/Internal/Type.hs @@ -0,0 +1,30 @@ +module Internal.Type (substType) where + +import Data.Maybe (fromMaybe) +import GhcPlugins hiding (TcPlugin, mkSubst) +import TcType (TcType) +import TyCoRep (Type (..)) + +-- | 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 af t1 t2) = + FunTy af (substType subst t1) (substType subst t2) +substType _ l@(LitTy _) = l +substType subst (CastTy ty co) = + CastTy (substType subst ty) co +substType _ co@(CoercionTy _) = co diff --git a/src-ghc-8.2/GhcApi/GhcPlugins.hs b/src-ghc-8.2/GhcApi/GhcPlugins.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.2/GhcApi/GhcPlugins.hs @@ -0,0 +1,5 @@ +module GhcApi.GhcPlugins (module GhcPlugins, TcTyVar, EvTerm(..)) where + +import GhcPlugins hiding (mkSubst) +import TcType (TcTyVar) +import TcEvidence (EvTerm(..)) diff --git a/src-ghc-8.2/Internal/Constraint.hs b/src-ghc-8.2/Internal/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.2/Internal/Constraint.hs @@ -0,0 +1,26 @@ +module Internal.Constraint (module TcPluginM, flatToCt, overEvidencePredType) where + +import GhcApi.GhcPlugins +import GhcApi.Constraint + (Ct(..), CtEvidence(..), ctLoc, ctEvId, mkNonCanonical) + +import TcType (TcType) +import TcPluginM (newGiven) + +flatToCt :: [((TcTyVar,TcType),Ct)] -> Maybe Ct +flatToCt [((_,lhs),ct),((_,rhs),_)] + = Just + $ mkNonCanonical + $ CtGiven (mkPrimEqPred lhs rhs) + (ctEvId (cc_ev ct)) + (ctLoc ct) + +flatToCt _ = Nothing + +-- | Modify the predicate type of the evidence term of a constraint +overEvidencePredType :: (TcType -> TcType) -> Ct -> Ct +overEvidencePredType f ct = + let + ev :: CtEvidence + ev = cc_ev ct + in ct { cc_ev = ev { ctev_pred = f (ctev_pred ev) } } diff --git a/src-ghc-8.2/Internal/Evidence.hs b/src-ghc-8.2/Internal/Evidence.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.2/Internal/Evidence.hs @@ -0,0 +1,24 @@ +module Internal.Evidence (evByFiat, evByFiatWithDependencies) where + +import TcEvidence (EvTerm(..)) +import TyCoRep (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 = + EvCoercion $ mkUnivCo (PluginProv name) Nominal t1 t2 + +-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce' +evByFiatWithDependencies :: + String -- ^ Name the coercion should have + -> [Coercion] -- ^ The set of all the in-scope coercion 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 = + EvCoercion $ mkUnivCo (PluginProv name) Nominal t1 t2 diff --git a/src-ghc-8.2/Internal/Type.hs b/src-ghc-8.2/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.2/Internal/Type.hs @@ -0,0 +1,29 @@ +module Internal.Type (substType) where + +import Data.Maybe (fromMaybe) +import TcType (TcTyVar, TcType) +import TyCoRep (Type (..)) + +-- | 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 t1 t2) = + FunTy (substType subst t1) (substType subst t2) +substType _ l@(LitTy _) = l +substType subst (CastTy ty co) = + CastTy (substType subst ty) co +substType _ co@(CoercionTy _) = co diff --git a/src-ghc-8.4/GhcApi/GhcPlugins.hs b/src-ghc-8.4/GhcApi/GhcPlugins.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.4/GhcApi/GhcPlugins.hs @@ -0,0 +1,5 @@ +module GhcApi.GhcPlugins (module GhcPlugins, TcTyVar, EvTerm(..)) where + +import GhcPlugins hiding (mkSubst) +import TcType (TcTyVar) +import TcEvidence (EvTerm(..)) diff --git a/src-ghc-8.4/Internal/Constraint.hs b/src-ghc-8.4/Internal/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.4/Internal/Constraint.hs @@ -0,0 +1,26 @@ +module Internal.Constraint (module TcPluginM, flatToCt, overEvidencePredType) where + +import GhcApi.GhcPlugins +import GhcApi.Constraint + (Ct(..), CtEvidence(..), ctLoc, ctEvId, mkNonCanonical) + +import TcType (TcType) +import TcPluginM (newGiven) + +flatToCt :: [((TcTyVar,TcType),Ct)] -> Maybe Ct +flatToCt [((_,lhs),ct),((_,rhs),_)] + = Just + $ mkNonCanonical + $ CtGiven (mkPrimEqPred lhs rhs) + (ctEvId ct) + (ctLoc ct) + +flatToCt _ = Nothing + +-- | Modify the predicate type of the evidence term of a constraint +overEvidencePredType :: (TcType -> TcType) -> Ct -> Ct +overEvidencePredType f ct = + let + ev :: CtEvidence + ev = cc_ev ct + in ct { cc_ev = ev { ctev_pred = f (ctev_pred ev) } } diff --git a/src-ghc-8.4/Internal/Evidence.hs b/src-ghc-8.4/Internal/Evidence.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.4/Internal/Evidence.hs @@ -0,0 +1,24 @@ +module Internal.Evidence (evByFiat, evByFiatWithDependencies) where + +import TcEvidence (EvTerm(..)) +import TyCoRep (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 = + EvCoercion $ mkUnivCo (PluginProv name) Nominal t1 t2 + +-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce' +evByFiatWithDependencies :: + String -- ^ Name the coercion should have + -> [Coercion] -- ^ The set of all the in-scope coercion 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 = + EvCoercion $ mkUnivCo (PluginProv name) Nominal t1 t2 diff --git a/src-ghc-8.4/Internal/Type.hs b/src-ghc-8.4/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.4/Internal/Type.hs @@ -0,0 +1,29 @@ +module Internal.Type (substType) where + +import Data.Maybe (fromMaybe) +import TcType (TcTyVar, TcType) +import TyCoRep (Type (..)) + +-- | 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 t1 t2) = + FunTy (substType subst t1) (substType subst t2) +substType _ l@(LitTy _) = l +substType subst (CastTy ty co) = + CastTy (substType subst ty) co +substType _ co@(CoercionTy _) = co diff --git a/src-ghc-8.6/GhcApi/GhcPlugins.hs b/src-ghc-8.6/GhcApi/GhcPlugins.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.6/GhcApi/GhcPlugins.hs @@ -0,0 +1,3 @@ +module GhcApi.GhcPlugins (module GhcPlugins) where + +import GhcPlugins hiding (mkSubst) diff --git a/src-ghc-8.6/Internal/Constraint.hs b/src-ghc-8.6/Internal/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.6/Internal/Constraint.hs @@ -0,0 +1,43 @@ +module Internal.Constraint (newGiven, flatToCt, overEvidencePredType) where + +import GhcApi.GhcPlugins +import GhcApi.Constraint + (Ct(..), CtEvidence(..), CtLoc, ctLoc, ctEvId, mkNonCanonical) + +import Panic (panicDoc) +import TcType (TcType) +import Constraint (QCInst(..)) +import TcEvidence (EvTerm(..)) +import TcPluginM (TcPluginM) +import qualified TcPluginM (newGiven) +import Outputable (ppr) +import Type (PredType) + +-- | 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 loc pty (EvExpr ev) = TcPluginM.newGiven 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 + +-- | Modify the predicate type of the evidence term of a constraint +overEvidencePredType :: (TcType -> TcType) -> Ct -> Ct +overEvidencePredType f (CQuantCan qci) = + let + ev :: CtEvidence + ev = qci_ev qci + in CQuantCan ( qci { qci_ev = ev { ctev_pred = f (ctev_pred ev) } } ) +overEvidencePredType f ct = + let + ev :: CtEvidence + ev = cc_ev ct + in ct { cc_ev = ev { ctev_pred = f (ctev_pred ev) } } diff --git a/src-ghc-8.6/Internal/Evidence.hs b/src-ghc-8.6/Internal/Evidence.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.6/Internal/Evidence.hs @@ -0,0 +1,24 @@ +module Internal.Evidence (evByFiat, evByFiatWithDependencies) where + +import TcEvidence (EvTerm(..)) +import TyCoRep (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) Nominal t1 t2 + +-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce' +evByFiatWithDependencies :: + String -- ^ Name the coercion should have + -> [Coercion] -- ^ The set of all the in-scope coercion 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) Nominal t1 t2 diff --git a/src-ghc-8.6/Internal/Type.hs b/src-ghc-8.6/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.6/Internal/Type.hs @@ -0,0 +1,30 @@ +module Internal.Type (substType) where + +import Data.Maybe (fromMaybe) +import GhcPlugins hiding (mkSubst) +import TcType (TcType) +import TyCoRep (Type (..)) + +-- | 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 t1 t2) = + FunTy (substType subst t1) (substType subst t2) +substType _ l@(LitTy _) = l +substType subst (CastTy ty co) = + CastTy (substType subst ty) co +substType _ co@(CoercionTy _) = co diff --git a/src-ghc-8.8/GhcApi/GhcPlugins.hs b/src-ghc-8.8/GhcApi/GhcPlugins.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.8/GhcApi/GhcPlugins.hs @@ -0,0 +1,3 @@ +module GhcApi.GhcPlugins (module GhcPlugins) where + +import GhcPlugins hiding (TcPlugin, mkSubst) diff --git a/src-ghc-8.8/Internal/Constraint.hs b/src-ghc-8.8/Internal/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.8/Internal/Constraint.hs @@ -0,0 +1,41 @@ +module Internal.Constraint (newGiven, flatToCt, overEvidencePredType) where + +import GhcApi.GhcPlugins +import GhcApi.Constraint + (Ct(..), CtEvidence(..), CtLoc, ctLoc, ctEvId, mkNonCanonical) + +import Panic (panicDoc) +import TcType (TcType) +import Constraint (QCInst(..)) +import TcEvidence (EvTerm(..)) +import TcPluginM (TcPluginM) +import qualified TcPluginM (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 loc pty (EvExpr ev) = TcPluginM.newGiven 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 + +-- | Modify the predicate type of the evidence term of a constraint +overEvidencePredType :: (TcType -> TcType) -> Ct -> Ct +overEvidencePredType f (CQuantCan qci) = + let + ev :: CtEvidence + ev = qci_ev qci + in CQuantCan ( qci { qci_ev = ev { ctev_pred = f (ctev_pred ev) } } ) +overEvidencePredType f ct = + let + ev :: CtEvidence + ev = cc_ev ct + in ct { cc_ev = ev { ctev_pred = f (ctev_pred ev) } } diff --git a/src-ghc-8.8/Internal/Evidence.hs b/src-ghc-8.8/Internal/Evidence.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.8/Internal/Evidence.hs @@ -0,0 +1,24 @@ +module Internal.Evidence (evByFiat, evByFiatWithDependencies) where + +import TcEvidence (EvTerm(..)) +import TyCoRep (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) Nominal t1 t2 + +-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce' +evByFiatWithDependencies :: + String -- ^ Name the coercion should have + -> [Coercion] -- ^ The set of all the in-scope coercion 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) Nominal t1 t2 diff --git a/src-ghc-8.8/Internal/Type.hs b/src-ghc-8.8/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src-ghc-8.8/Internal/Type.hs @@ -0,0 +1,30 @@ +module Internal.Type (substType) where + +import Data.Maybe (fromMaybe) +import GhcPlugins hiding (TcPlugin, mkSubst) +import TcType (TcType) +import TyCoRep (Type (..)) + +-- | 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 t1 t2) = + FunTy (substType subst t1) (substType subst t2) +substType _ l@(LitTy _) = l +substType subst (CastTy ty co) = + CastTy (substType subst ty) co +substType _ co@(CoercionTy _) = co diff --git a/src-ghc-9.0/GhcApi/Constraint.hs b/src-ghc-9.0/GhcApi/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.0/GhcApi/Constraint.hs @@ -0,0 +1,12 @@ +module GhcApi.Constraint + ( Ct(..) + , CtEvidence(..) + , CtLoc + , ctLoc + , ctEvId + , mkNonCanonical + ) +where + +import GHC.Tc.Types.Constraint + (Ct (..), CtEvidence (..), CtLoc, ctLoc, ctEvId, mkNonCanonical) diff --git a/src-ghc-9.0/GhcApi/GhcPlugins.hs b/src-ghc-9.0/GhcApi/GhcPlugins.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.0/GhcApi/GhcPlugins.hs @@ -0,0 +1,5 @@ +module GhcApi.GhcPlugins (module GHC.Plugins, findPluginModule, panicDoc) where + +import GHC.Plugins hiding (TcPlugin, mkSubst) +import GHC.Driver.Finder (findPluginModule) +import GHC.Utils.Panic (panicDoc) diff --git a/src-ghc-9.0/Internal/Constraint.hs b/src-ghc-9.0/Internal/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.0/Internal/Constraint.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE RecordWildCards #-} + +module Internal.Constraint (newGiven, flatToCt, mkSubst, overEvidencePredType) where + +import GhcApi.GhcPlugins +import GhcApi.Constraint + (Ct(..), CtEvidence(..), CtLoc, ctLoc, ctEvId, mkNonCanonical) + +import GHC.Tc.Utils.TcType (TcType) +import GHC.Core.TyCo.Rep (Type (..)) +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 loc pty (EvExpr ev) = TcPlugin.newGiven 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@(CTyEqCan {..}) = Just ((cc_tyvar,cc_rhs),ct) +mkSubst ct@(CFunEqCan {..}) = Just ((cc_fsk,TyConApp cc_fun cc_tyargs),ct) +mkSubst _ = Nothing + +-- | Modify the predicate type of the evidence term of a constraint +overEvidencePredType :: (TcType -> TcType) -> Ct -> Ct +overEvidencePredType f (CQuantCan qci) = + let + ev :: CtEvidence + ev = qci_ev qci + in CQuantCan ( qci { qci_ev = ev { ctev_pred = f (ctev_pred ev) } } ) +overEvidencePredType f ct = + let + ev :: CtEvidence + ev = cc_ev ct + in ct { cc_ev = ev { ctev_pred = f (ctev_pred ev) } } diff --git a/src-ghc-9.0/Internal/Evidence.hs b/src-ghc-9.0/Internal/Evidence.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.0/Internal/Evidence.hs @@ -0,0 +1,24 @@ +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) Nominal t1 t2 + +-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce' +evByFiatWithDependencies :: + String -- ^ Name the coercion should have + -> [Coercion] -- ^ The set of all the in-scope coercion 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) Nominal t1 t2 diff --git a/src-ghc-9.0/Internal/Type.hs b/src-ghc-9.0/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.0/Internal/Type.hs @@ -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 diff --git a/src-ghc-9.10/GhcApi/Constraint.hs b/src-ghc-9.10/GhcApi/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.10/GhcApi/Constraint.hs @@ -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) diff --git a/src-ghc-9.10/GhcApi/GhcPlugins.hs b/src-ghc-9.10/GhcApi/GhcPlugins.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.10/GhcApi/GhcPlugins.hs @@ -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(..)) diff --git a/src-ghc-9.10/Internal/Constraint.hs b/src-ghc-9.10/Internal/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.10/Internal/Constraint.hs @@ -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) } } ) diff --git a/src-ghc-9.10/Internal/Evidence.hs b/src-ghc-9.10/Internal/Evidence.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.10/Internal/Evidence.hs @@ -0,0 +1,24 @@ +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) Nominal t1 t2 + +-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce' +evByFiatWithDependencies :: + String -- ^ Name the coercion should have + -> [Coercion] -- ^ The set of all the in-scope coercion 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) Nominal t1 t2 diff --git a/src-ghc-9.10/Internal/Type.hs b/src-ghc-9.10/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.10/Internal/Type.hs @@ -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 diff --git a/src-ghc-9.12/GhcApi/Constraint.hs b/src-ghc-9.12/GhcApi/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.12/GhcApi/Constraint.hs @@ -0,0 +1,14 @@ +module GhcApi.Constraint + ( Ct(..) + , CtEvidence(..) + , CtLoc + , CanEqLHS(..) + , ctLoc + , ctEvId + , mkNonCanonical + ) +where + +import GHC.Tc.Types.Constraint + (Ct (..), CtEvidence (..), CanEqLHS (..), ctLoc, ctEvId, mkNonCanonical) +import GHC.Tc.Types.CtLoc (CtLoc) diff --git a/src-ghc-9.12/GhcApi/GhcPlugins.hs b/src-ghc-9.12/GhcApi/GhcPlugins.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.12/GhcApi/GhcPlugins.hs @@ -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(..)) diff --git a/src-ghc-9.12/Internal/Constraint.hs b/src-ghc-9.12/Internal/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.12/Internal/Constraint.hs @@ -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) } } ) diff --git a/src-ghc-9.12/Internal/Evidence.hs b/src-ghc-9.12/Internal/Evidence.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.12/Internal/Evidence.hs @@ -0,0 +1,25 @@ +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) [] 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 + -> [Coercion] -- ^ The set of all the in-scope coercion 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 diff --git a/src-ghc-9.12/Internal/Type.hs b/src-ghc-9.12/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.12/Internal/Type.hs @@ -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 diff --git a/src-ghc-9.2/GhcApi/Constraint.hs b/src-ghc-9.2/GhcApi/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.2/GhcApi/Constraint.hs @@ -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) diff --git a/src-ghc-9.2/GhcApi/GhcPlugins.hs b/src-ghc-9.2/GhcApi/GhcPlugins.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.2/GhcApi/GhcPlugins.hs @@ -0,0 +1,5 @@ +module GhcApi.GhcPlugins (module GHC.Plugins, FindResult(..), findPluginModule) where + +import GHC.Plugins hiding (TcPlugin, mkSubst) +import GHC.Unit.Finder (findPluginModule) +import GHC.Tc.Plugin (FindResult(..)) diff --git a/src-ghc-9.2/Internal/Constraint.hs b/src-ghc-9.2/Internal/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.2/Internal/Constraint.hs @@ -0,0 +1,49 @@ +{-# 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 loc pty (EvExpr ev) = TcPlugin.newGiven 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 {..}) + | TyVarLHS tyvar <- cc_lhs + = Just ((tyvar,cc_rhs),ct) +mkSubst _ = Nothing + +-- | Modify the predicate type of the evidence term of a constraint +overEvidencePredType :: (TcType -> TcType) -> Ct -> Ct +overEvidencePredType f (CQuantCan qci) = + let + ev :: CtEvidence + ev = qci_ev qci + in CQuantCan ( qci { qci_ev = ev { ctev_pred = f (ctev_pred ev) } } ) +overEvidencePredType f ct = + let + ev :: CtEvidence + ev = cc_ev ct + in ct { cc_ev = ev { ctev_pred = f (ctev_pred ev) } } diff --git a/src-ghc-9.2/Internal/Evidence.hs b/src-ghc-9.2/Internal/Evidence.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.2/Internal/Evidence.hs @@ -0,0 +1,24 @@ +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) Nominal t1 t2 + +-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce' +evByFiatWithDependencies :: + String -- ^ Name the coercion should have + -> [Coercion] -- ^ The set of all the in-scope coercion 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) Nominal t1 t2 diff --git a/src-ghc-9.2/Internal/Type.hs b/src-ghc-9.2/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.2/Internal/Type.hs @@ -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 diff --git a/src-ghc-9.4/GhcApi/Constraint.hs b/src-ghc-9.4/GhcApi/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.4/GhcApi/Constraint.hs @@ -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) diff --git a/src-ghc-9.4/GhcApi/GhcPlugins.hs b/src-ghc-9.4/GhcApi/GhcPlugins.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.4/GhcApi/GhcPlugins.hs @@ -0,0 +1,5 @@ +module GhcApi.GhcPlugins (module GHC.Plugins, FindResult(..), findPluginModule) where + +import GHC.Plugins hiding (TcPlugin, mkSubst) +import GHC.Unit.Finder (findPluginModule) +import GHC.Tc.Plugin (FindResult(..)) diff --git a/src-ghc-9.4/Internal/Constraint.hs b/src-ghc-9.4/Internal/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.4/Internal/Constraint.hs @@ -0,0 +1,49 @@ +{-# 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 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 {..}) + | TyVarLHS tyvar <- cc_lhs + = Just ((tyvar,cc_rhs),ct) +mkSubst _ = Nothing + +-- | Modify the predicate type of the evidence term of a constraint +overEvidencePredType :: (TcType -> TcType) -> Ct -> Ct +overEvidencePredType f (CQuantCan qci) = + let + ev :: CtEvidence + ev = qci_ev qci + in CQuantCan ( qci { qci_ev = ev { ctev_pred = f (ctev_pred ev) } } ) +overEvidencePredType f ct = + let + ev :: CtEvidence + ev = cc_ev ct + in ct { cc_ev = ev { ctev_pred = f (ctev_pred ev) } } diff --git a/src-ghc-9.4/Internal/Evidence.hs b/src-ghc-9.4/Internal/Evidence.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.4/Internal/Evidence.hs @@ -0,0 +1,24 @@ +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) Nominal t1 t2 + +-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce' +evByFiatWithDependencies :: + String -- ^ Name the coercion should have + -> [Coercion] -- ^ The set of all the in-scope coercion 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) Nominal t1 t2 diff --git a/src-ghc-9.4/Internal/Type.hs b/src-ghc-9.4/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.4/Internal/Type.hs @@ -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 diff --git a/src-ghc-9.8/GhcApi/Constraint.hs b/src-ghc-9.8/GhcApi/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.8/GhcApi/Constraint.hs @@ -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) diff --git a/src-ghc-9.8/GhcApi/GhcPlugins.hs b/src-ghc-9.8/GhcApi/GhcPlugins.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.8/GhcApi/GhcPlugins.hs @@ -0,0 +1,5 @@ +module GhcApi.GhcPlugins (module GHC.Plugins, FindResult(..), findPluginModule) where + +import GHC.Plugins hiding (TcPlugin, mkSubst) +import GHC.Unit.Finder (findPluginModule) +import GHC.Tc.Plugin (FindResult(..)) diff --git a/src-ghc-9.8/Internal/Constraint.hs b/src-ghc-9.8/Internal/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.8/Internal/Constraint.hs @@ -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) } } ) diff --git a/src-ghc-9.8/Internal/Evidence.hs b/src-ghc-9.8/Internal/Evidence.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.8/Internal/Evidence.hs @@ -0,0 +1,24 @@ +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) Nominal t1 t2 + +-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce' +evByFiatWithDependencies :: + String -- ^ Name the coercion should have + -> [Coercion] -- ^ The set of all the in-scope coercion 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) Nominal t1 t2 diff --git a/src-ghc-9.8/Internal/Type.hs b/src-ghc-9.8/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.8/Internal/Type.hs @@ -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 diff --git a/src-ghc-flat/GhcApi/Constraint.hs b/src-ghc-flat/GhcApi/Constraint.hs new file mode 100644 --- /dev/null +++ b/src-ghc-flat/GhcApi/Constraint.hs @@ -0,0 +1,12 @@ +module GhcApi.Constraint + ( Ct(..) + , CtEvidence(..) + , CtLoc + , ctLoc + , ctEvId + , mkNonCanonical + ) +where + +import Constraint + (Ct (..), CtEvidence (..), CtLoc, ctLoc, ctEvId, mkNonCanonical) diff --git a/src-ghc-flat/GhcApi/Predicate.hs b/src-ghc-flat/GhcApi/Predicate.hs new file mode 100644 --- /dev/null +++ b/src-ghc-flat/GhcApi/Predicate.hs @@ -0,0 +1,3 @@ +module GhcApi.Predicate (mkPrimEqPred) where + +import Predicate (mkPrimEqPred) diff --git a/src-ghc-flat/Internal.hs b/src-ghc-flat/Internal.hs new file mode 100644 --- /dev/null +++ b/src-ghc-flat/Internal.hs @@ -0,0 +1,152 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE PatternSynonyms #-} + +{-# OPTIONS_HADDOCK show-extensions #-} + +module Internal + ( -- * Create new constraints + newWanted + , newGiven + , newDerived + -- * Creating evidence + , evByFiatWithDependencies + , evByFiat + -- * Lookup + , lookupModule + , lookupName + -- * Trace state of the plugin + , tracePlugin + -- * Substitutions + , flattenGivens + , mkSubst + , mkSubst' + , substType + , substCt + ) +where + +import Panic (panicDoc) +import TcPluginM (TcPluginM, lookupOrig, tcPluginTrace) +import qualified TcPluginM +import qualified Finder +import TcRnTypes (TcPlugin(..), TcPluginResult(..)) +import Control.Arrow (first, second) +import Data.Function (on) +import Data.List (groupBy, partition, sortOn) +import TcType (TcType) +import Data.Maybe (mapMaybe) +import TyCoRep (Type(..)) + +import GhcApi.Constraint (Ct(..), CtEvidence(..), CtLoc) +import GhcApi.GhcPlugins + +import Internal.Type (substType) +import Internal.Constraint (newGiven, flatToCt, overEvidencePredType) +import Internal.Evidence (evByFiat, evByFiatWithDependencies) + +{-# ANN fr_mod "HLint: ignore Use camelCase" #-} + +pattern FoundModule :: Module -> FindResult +pattern FoundModule a <- Found _ a + +fr_mod :: a -> a +fr_mod = id + +-- | Create a new [W]anted constraint. +newWanted :: CtLoc -> PredType -> TcPluginM CtEvidence +newWanted = TcPluginM.newWanted + +-- | Create a new [D]erived constraint. +newDerived :: CtLoc -> PredType -> TcPluginM CtEvidence +newDerived = TcPluginM.newDerived + +-- | Find a module +lookupModule :: ModuleName -- ^ Name of the module + -> FastString -- ^ Name of the package containing the module. + -- NOTE: This value is ignored on ghc>=8.0. + -> TcPluginM Module +lookupModule mod_nm _pkg = do + hsc_env <- TcPluginM.getTopEnv + found_module <- TcPluginM.tcPluginIO $ Finder.findPluginModule hsc_env mod_nm + case found_module of + FoundModule h -> return (fr_mod h) + _ -> do + found_module' <- TcPluginM.findImportedModule mod_nm $ Just $ fsLit "this" + case found_module' of + FoundModule h -> return (fr_mod h) + _ -> panicDoc "Couldn't find module" (ppr mod_nm) + +-- | Find a 'Name' in a 'Module' given an 'OccName' +lookupName :: Module -> OccName -> TcPluginM Name +lookupName = lookupOrig + +-- | Print out extra information about the initialisation, stop, and every run +-- of the plugin when @-ddump-tc-trace@ is enabled. +tracePlugin :: String -> TcPlugin -> TcPlugin +tracePlugin s TcPlugin{..} = TcPlugin { tcPluginInit = traceInit + , tcPluginSolve = traceSolve + , tcPluginStop = traceStop + } + where + traceInit = do + -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301 + initializeStaticFlags + tcPluginTrace ("tcPluginInit " ++ s) empty >> tcPluginInit + + traceStop z = tcPluginTrace ("tcPluginStop " ++ s) empty >> tcPluginStop z + + traceSolve z given derived wanted = do + tcPluginTrace ("tcPluginSolve start " ++ s) + (text "given =" <+> ppr given + $$ text "derived =" <+> ppr derived + $$ text "wanted =" <+> ppr wanted) + r <- tcPluginSolve z given derived wanted + case r of + TcPluginOk solved new -> tcPluginTrace ("tcPluginSolve ok " ++ s) + (text "solved =" <+> ppr solved + $$ text "new =" <+> ppr new) + TcPluginContradiction bad -> tcPluginTrace + ("tcPluginSolve contradiction " ++ s) + (text "bad =" <+> ppr bad) + return r + +-- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301 +initializeStaticFlags :: TcPluginM () +initializeStaticFlags = return () + +-- | Flattens evidence of constraints by substituting each others equalities. +-- +-- __NB:__ Should only be used on /[G]iven/ constraints! +-- +-- __NB:__ Doesn't flatten under binders +flattenGivens :: [Ct] -> [Ct] +flattenGivens givens = + mapMaybe flatToCt flat ++ map (substCt subst') givens + where + subst = mkSubst' givens + (flat,subst') + = second (map fst . concat) + $ partition ((>= 2) . length) + $ groupBy ((==) `on` (fst.fst)) + $ sortOn (fst.fst) subst + +-- | Create flattened substitutions from type equalities, i.e. the substitutions +-- have been applied to each others right hand sides. +mkSubst' :: [Ct] -> [((TcTyVar,TcType),Ct)] +mkSubst' = foldr substSubst [] . mapMaybe mkSubst + where + substSubst :: ((TcTyVar,TcType),Ct) + -> [((TcTyVar,TcType),Ct)] + -> [((TcTyVar,TcType),Ct)] + substSubst ((tv,t),ct) s = ((tv,substType (map fst s) t),ct) + : map (first (second (substType [(tv,t)]))) s + +-- | Create simple substitution from type equalities +mkSubst :: Ct -> Maybe ((TcTyVar, TcType),Ct) +mkSubst ct@CTyEqCan{..} = Just ((cc_tyvar,cc_rhs),ct) +mkSubst ct@CFunEqCan{..} = Just ((cc_fsk,TyConApp cc_fun cc_tyargs),ct) +mkSubst _ = Nothing + +-- | Apply substitution in the evidence of Cts +substCt :: [(TcTyVar, TcType)] -> Ct -> Ct +substCt subst = overEvidencePredType (substType subst) diff --git a/src-ghc-tree-9.4/GhcApi/Predicate.hs b/src-ghc-tree-9.4/GhcApi/Predicate.hs new file mode 100644 --- /dev/null +++ b/src-ghc-tree-9.4/GhcApi/Predicate.hs @@ -0,0 +1,3 @@ +module GhcApi.Predicate (mkPrimEqPred) where + +import GHC.Core.Coercion (mkPrimEqPred) diff --git a/src-ghc-tree-9.4/Internal.hs b/src-ghc-tree-9.4/Internal.hs new file mode 100644 --- /dev/null +++ b/src-ghc-tree-9.4/Internal.hs @@ -0,0 +1,134 @@ +{-# LANGUAGE RecordWildCards #-} + +{-# OPTIONS_HADDOCK show-extensions #-} + +module Internal + ( -- * Create new constraints + TcPlugin.newWanted + , newGiven + -- * Creating evidence + , evByFiatWithDependencies + , evByFiat + -- * Lookup + , lookupModule + , lookupName + -- * Trace state of the plugin + , tracePlugin + -- * Substitutions + , flattenGivens + , mkSubst + , mkSubst' + , substType + , substCt + ) +where + +import GHC.Driver.Config.Finder (initFinderOpts) +import GHC.Tc.Plugin (TcPluginM, lookupOrig, tcPluginTrace) +import qualified GHC.Tc.Plugin as TcPlugin + (newWanted, getTopEnv, tcPluginIO, findImportedModule) +import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult(..)) +import Control.Arrow (first, second) +import Data.Function (on) +import Data.List (groupBy, partition, sortOn) +import GHC.Tc.Utils.TcType (TcType) +import Data.Maybe (mapMaybe) + +import GhcApi.Constraint (Ct(..)) +import GhcApi.GhcPlugins + +import Internal.Type (substType) +import Internal.Constraint (newGiven, flatToCt, mkSubst, overEvidencePredType) +import Internal.Evidence (evByFiatWithDependencies, evByFiat) + +-- | Find a module +lookupModule :: ModuleName -- ^ Name of the module + -> FastString -- ^ Name of the package containing the module. + -- NOTE: This value is ignored on ghc>=8.0. + -> TcPluginM Module +lookupModule mod_nm _pkg = do + hsc_env <- TcPlugin.getTopEnv + let fc = hsc_FC hsc_env + dflags = hsc_dflags hsc_env + fopts = initFinderOpts dflags + units = hsc_units hsc_env + mhome_unit = hsc_home_unit_maybe hsc_env + found_module <- TcPlugin.tcPluginIO $ findPluginModule fc fopts units + mhome_unit mod_nm + case found_module of + Found _ h -> return h + _ -> do + let pkg_qual = maybe NoPkgQual (ThisPkg . homeUnitId) mhome_unit + found_module' <- TcPlugin.findImportedModule mod_nm pkg_qual + case found_module' of + Found _ h -> return h + _ -> panicDoc "Couldn't find module" (ppr mod_nm) + +-- | Find a 'Name' in a 'Module' given an 'OccName' +lookupName :: Module -> OccName -> TcPluginM Name +lookupName = lookupOrig + +-- | Print out extra information about the initialisation, stop, and every run +-- of the plugin when @-ddump-tc-trace@ is enabled. +tracePlugin :: String -> TcPlugin -> TcPlugin +tracePlugin s TcPlugin{..} = TcPlugin { tcPluginInit = traceInit + , tcPluginSolve = traceSolve + , tcPluginRewrite = tcPluginRewrite + , tcPluginStop = traceStop + } + where + traceInit = do + tcPluginTrace ("tcPluginInit " ++ s) empty >> tcPluginInit + + traceStop z = tcPluginTrace ("tcPluginStop " ++ s) empty >> tcPluginStop z + + traceSolve z ev given wanted = do + tcPluginTrace ("tcPluginSolve start " ++ s) + (text "given =" <+> ppr given + $$ text "wanted =" <+> ppr wanted) + r <- tcPluginSolve z ev given wanted + case r of + TcPluginOk solved new + -> tcPluginTrace ("tcPluginSolve ok " ++ s) + (text "solved =" <+> ppr solved + $$ text "new =" <+> ppr new) + TcPluginContradiction bad + -> tcPluginTrace ("tcPluginSolve contradiction " ++ s) + (text "bad =" <+> ppr bad) + TcPluginSolveResult bad solved new + -> tcPluginTrace ("tcPluginSolveResult " ++ s) + (text "solved =" <+> ppr solved + $$ text "bad =" <+> ppr bad + $$ text "new =" <+> ppr new) + return r + +-- | Flattens evidence of constraints by substituting each others equalities. +-- +-- __NB:__ Should only be used on /[G]iven/ constraints! +-- +-- __NB:__ Doesn't flatten under binders +flattenGivens :: [Ct] -> [Ct] +flattenGivens givens = + mapMaybe flatToCt flat ++ map (substCt subst') givens + where + subst = mkSubst' givens + (flat,subst') + = second (map fst . concat) + $ partition ((>= 2) . length) + $ groupBy ((==) `on` (fst.fst)) + $ sortOn (fst.fst) subst + +-- | Create flattened substitutions from type equalities, i.e. the substitutions +-- have been applied to each others right hand sides. +mkSubst' :: [Ct] -> [((TcTyVar,TcType),Ct)] +mkSubst' = foldr substSubst [] . mapMaybe mkSubst + where + substSubst :: ((TcTyVar,TcType),Ct) + -> [((TcTyVar,TcType),Ct)] + -> [((TcTyVar,TcType),Ct)] + substSubst ((tv,t),ct) s = ((tv,substType (map fst s) t),ct) + : map (first (second (substType [(tv,t)]))) s + +-- | Apply substitution in the evidence of Cts +substCt :: [(TcTyVar, TcType)] -> Ct -> Ct +substCt subst = overEvidencePredType (substType subst) diff --git a/src-ghc-tree/GhcApi/Predicate.hs b/src-ghc-tree/GhcApi/Predicate.hs new file mode 100644 --- /dev/null +++ b/src-ghc-tree/GhcApi/Predicate.hs @@ -0,0 +1,3 @@ +module GhcApi.Predicate (mkPrimEqPred) where + +import GHC.Core.Coercion (mkPrimEqPred) diff --git a/src-ghc-tree/Internal.hs b/src-ghc-tree/Internal.hs new file mode 100644 --- /dev/null +++ b/src-ghc-tree/Internal.hs @@ -0,0 +1,144 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE PatternSynonyms #-} + +{-# OPTIONS_HADDOCK show-extensions #-} + +module Internal + ( -- * Create new constraints + newWanted + , newGiven + , newDerived + -- * Creating evidence + , evByFiatWithDependencies + , evByFiat + -- * Lookup + , lookupModule + , lookupName + -- * Trace state of the plugin + , tracePlugin + -- * Substitutions + , flattenGivens + , mkSubst + , mkSubst' + , substType + , substCt + ) +where + +import GHC.Tc.Plugin (TcPluginM, lookupOrig, tcPluginTrace) +import qualified GHC.Tc.Plugin as TcPlugin + (newDerived, newWanted, getTopEnv, tcPluginIO, findImportedModule) +import GHC.Tc.Types (TcPlugin(..), TcPluginResult(..)) +import Control.Arrow (first, second) +import Data.Function (on) +import Data.List (groupBy, partition, sortOn) +import GHC.Tc.Utils.TcType (TcType) +import Data.Maybe (mapMaybe) + +import GhcApi.Constraint (Ct(..), CtEvidence(..), CtLoc) +import GhcApi.GhcPlugins + +import Internal.Type (substType) +import Internal.Constraint (newGiven, flatToCt, mkSubst, overEvidencePredType) +import Internal.Evidence (evByFiat, evByFiatWithDependencies) + +{-# ANN fr_mod "HLint: ignore Use camelCase" #-} + +pattern FoundModule :: Module -> FindResult +pattern FoundModule a <- Found _ a + +fr_mod :: a -> a +fr_mod = id + +-- | Create a new [W]anted constraint. +newWanted :: CtLoc -> PredType -> TcPluginM CtEvidence +newWanted = TcPlugin.newWanted + +-- | Create a new [D]erived constraint. +newDerived :: CtLoc -> PredType -> TcPluginM CtEvidence +newDerived = TcPlugin.newDerived + +-- | Find a module +lookupModule :: ModuleName -- ^ Name of the module + -> FastString -- ^ Name of the package containing the module. + -- NOTE: This value is ignored on ghc>=8.0. + -> TcPluginM Module +lookupModule mod_nm _pkg = do + hsc_env <- TcPlugin.getTopEnv + found_module <- TcPlugin.tcPluginIO $ findPluginModule hsc_env mod_nm + case found_module of + FoundModule h -> return (fr_mod h) + _ -> do + found_module' <- TcPlugin.findImportedModule mod_nm $ Just $ fsLit "this" + case found_module' of + FoundModule h -> return (fr_mod h) + _ -> panicDoc "Couldn't find module" (ppr mod_nm) + +-- | Find a 'Name' in a 'Module' given an 'OccName' +lookupName :: Module -> OccName -> TcPluginM Name +lookupName = lookupOrig + +-- | Print out extra information about the initialisation, stop, and every run +-- of the plugin when @-ddump-tc-trace@ is enabled. +tracePlugin :: String -> TcPlugin -> TcPlugin +tracePlugin s TcPlugin{..} = TcPlugin { tcPluginInit = traceInit + , tcPluginSolve = traceSolve + , tcPluginStop = traceStop + } + where + traceInit = do + -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301 + initializeStaticFlags + tcPluginTrace ("tcPluginInit " ++ s) empty >> tcPluginInit + + traceStop z = tcPluginTrace ("tcPluginStop " ++ s) empty >> tcPluginStop z + + traceSolve z given derived wanted = do + tcPluginTrace ("tcPluginSolve start " ++ s) + (text "given =" <+> ppr given + $$ text "derived =" <+> ppr derived + $$ text "wanted =" <+> ppr wanted) + r <- tcPluginSolve z given derived wanted + case r of + TcPluginOk solved new -> tcPluginTrace ("tcPluginSolve ok " ++ s) + (text "solved =" <+> ppr solved + $$ text "new =" <+> ppr new) + TcPluginContradiction bad -> tcPluginTrace + ("tcPluginSolve contradiction " ++ s) + (text "bad =" <+> ppr bad) + return r + +-- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301 +initializeStaticFlags :: TcPluginM () +initializeStaticFlags = return () + +-- | Flattens evidence of constraints by substituting each others equalities. +-- +-- __NB:__ Should only be used on /[G]iven/ constraints! +-- +-- __NB:__ Doesn't flatten under binders +flattenGivens :: [Ct] -> [Ct] +flattenGivens givens = + mapMaybe flatToCt flat ++ map (substCt subst') givens + where + subst = mkSubst' givens + (flat,subst') + = second (map fst . concat) + $ partition ((>= 2) . length) + $ groupBy ((==) `on` (fst.fst)) + $ sortOn (fst.fst) subst + +-- | Create flattened substitutions from type equalities, i.e. the substitutions +-- have been applied to each others right hand sides. +mkSubst' :: [Ct] -> [((TcTyVar,TcType),Ct)] +mkSubst' = foldr substSubst [] . mapMaybe mkSubst + where + substSubst :: ((TcTyVar,TcType),Ct) + -> [((TcTyVar,TcType),Ct)] + -> [((TcTyVar,TcType),Ct)] + substSubst ((tv,t),ct) s = ((tv,substType (map fst s) t),ct) + : map (first (second (substType [(tv,t)]))) s + +-- | Apply substitution in the evidence of Cts +substCt :: [(TcTyVar, TcType)] -> Ct -> Ct +substCt subst = overEvidencePredType (substType subst) diff --git a/src/GHC/TcPluginM/Extra.hs b/src/GHC/TcPluginM/Extra.hs --- a/src/GHC/TcPluginM/Extra.hs +++ b/src/GHC/TcPluginM/Extra.hs @@ -3,10 +3,7 @@ License : BSD2 (see the file LICENSE) Maintainer : Christiaan Baaij -} -{-# LANGUAGE CPP #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE CPP #-} {-# OPTIONS_HADDOCK show-extensions #-} @@ -14,11 +11,14 @@ ( -- * Create new constraints newWanted , newGiven +#if __GLASGOW_HASKELL__ < 904 , newDerived +#endif #if __GLASGOW_HASKELL__ < 711 , newWantedWithProvenance #endif -- * Creating evidence + , evByFiatWithDependencies , evByFiat #if __GLASGOW_HASKELL__ < 711 -- * Report contractions @@ -29,376 +29,13 @@ , lookupName -- * Trace state of the plugin , tracePlugin -#if __GLASGOW_HASKELL__ >= 804 - -- * Substitutions (GHC 8.4+) + -- * Substitutions , flattenGivens , mkSubst , mkSubst' , substType , substCt -#endif ) where --- External -#if __GLASGOW_HASKELL__ < 711 -import Data.Maybe (mapMaybe) -#endif - --- GHC API -#if __GLASGOW_HASKELL__ < 711 -import BasicTypes (TopLevelFlag (..)) -#endif -#if MIN_VERSION_ghc(8,5,0) -import CoreSyn (Expr(..)) -#endif -import Coercion (Role (..), mkUnivCo) -import FastString (FastString, fsLit) -import Module (Module, ModuleName) -import Name (Name) -import OccName (OccName) -import Outputable (($$), (<+>), empty, ppr, text) -import Panic (panicDoc) -#if __GLASGOW_HASKELL__ >= 711 -import TcEvidence (EvTerm (..)) -#else -import TcEvidence (EvTerm (..), TcCoercion (..)) -import TcMType (newEvVar) -#endif -#if __GLASGOW_HASKELL__ < 711 -import TcPluginM (FindResult (..), TcPluginM, findImportedModule, lookupOrig, - tcPluginTrace, unsafeTcPluginTcM) -import TcRnTypes (Ct, CtEvidence (..), CtLoc, TcIdBinder (..), TcLclEnv (..), - TcPlugin (..), TcPluginResult (..), ctEvId, ctEvLoc, ctLoc, - ctLocEnv, mkNonCanonical, setCtLocEnv) -#else -import TcPluginM (FindResult (..), TcPluginM, lookupOrig, tcPluginTrace) -import qualified TcPluginM -import qualified Finder -#if __GLASGOW_HASKELL__ < 809 -import TcRnTypes (CtEvidence (..), CtLoc, - TcPlugin (..), TcPluginResult (..)) -#else -import TcRnTypes (TcPlugin (..), TcPluginResult (..)) -#endif -#endif -#if __GLASGOW_HASKELL__ < 802 -import TcPluginM (tcPluginIO) -#endif -#if __GLASGOW_HASKELL__ >= 711 -import TyCoRep (UnivCoProvenance (..)) -import Type (PredType, Type) -#else -import Type (EqRel (..), PredTree (..), PredType, Type, classifyPredType) -import Var (varType) -#endif -#if __GLASGOW_HASKELL__ >= 804 -import Control.Arrow (first, second) -import Data.Function (on) -import Data.List (groupBy, partition, sortOn) -import Data.Maybe (mapMaybe) -#if __GLASGOW_HASKELL__ < 809 -import TcRnTypes (Ct (..), ctLoc, ctEvId, mkNonCanonical) -#else -import Constraint - (Ct (..), CtEvidence (..), CtLoc, ctLoc, ctEvId, mkNonCanonical) -#endif -import TcType (TcTyVar, TcType) -#if __GLASGOW_HASKELL__ < 809 -import Type (mkPrimEqPred) -#else -import Predicate (mkPrimEqPred) -#endif -import TyCoRep (Type (..)) -#endif - --- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301 -#if __GLASGOW_HASKELL__ < 802 -import Data.IORef (readIORef) -import Control.Monad (unless) -import StaticFlags (initStaticOpts, v_opt_C_ready) -#endif - -#if __GLASGOW_HASKELL__ >= 711 -pattern FoundModule :: Module -> FindResult -pattern FoundModule a <- Found _ a -fr_mod :: a -> a -fr_mod = id -#endif - - -#if __GLASGOW_HASKELL__ < 711 -{-# DEPRECATED newWantedWithProvenance "No longer available in GHC 8.0+" #-} --- | Create a new [W]anted constraint that remembers from which wanted --- constraint it was derived -newWantedWithProvenance :: CtEvidence -- ^ Constraint from which the new - -- wanted is derived - -> PredType -- ^ The type of the new constraint - -> TcPluginM CtEvidence -newWantedWithProvenance ev@(CtWanted {}) p = do - let loc = ctEvLoc ev - env = ctLocEnv loc - id_ = ctEvId ev - env' = env {tcl_bndrs = (TcIdBndr id_ NotTopLevel):tcl_bndrs env} - loc' = setCtLocEnv loc env' - evVar <- unsafeTcPluginTcM $ newEvVar p - return CtWanted { ctev_pred = p - , ctev_evar = evVar - , ctev_loc = loc'} - -newWantedWithProvenance ev _ = - panicDoc "newWantedWithProvenance: not a Wanted: " (ppr ev) -#endif - --- | Create a new [W]anted constraint. -newWanted :: CtLoc -> PredType -> TcPluginM CtEvidence -#if __GLASGOW_HASKELL__ >= 711 -newWanted = TcPluginM.newWanted -#else -newWanted loc pty = do - new_ev <- unsafeTcPluginTcM $ newEvVar pty - return CtWanted { ctev_pred = pty - , ctev_evar = new_ev - , ctev_loc = loc - } -#endif - --- | 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 -#if MIN_VERSION_ghc(8,5,0) -newGiven loc pty (EvExpr ev) = TcPluginM.newGiven loc pty ev -newGiven _ _ ev = panicDoc "newGiven: not an EvExpr: " (ppr ev) -#elif __GLASGOW_HASKELL__ >= 711 -newGiven = TcPluginM.newGiven -#else -newGiven loc pty evtm = return - CtGiven { ctev_pred = pty - , ctev_evtm = evtm - , ctev_loc = loc - } -#endif - --- | Create a new [D]erived constraint. -newDerived :: CtLoc -> PredType -> TcPluginM CtEvidence -#if __GLASGOW_HASKELL__ >= 711 -newDerived = TcPluginM.newDerived -#else -newDerived loc pty = return - CtDerived { ctev_pred = pty - , ctev_loc = loc - } -#endif - --- | 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 = -#if MIN_VERSION_ghc(8,5,0) - EvExpr - $ Coercion -#else - EvCoercion -#if __GLASGOW_HASKELL__ < 711 - $ TcCoercion -#endif -#endif - $ mkUnivCo -#if __GLASGOW_HASKELL__ >= 711 - (PluginProv name) -#else - (fsLit name) -#endif - Nominal t1 t2 - -#if __GLASGOW_HASKELL__ < 711 -{-# DEPRECATED failWithProvenace "No longer available in GHC 8.0+" #-} --- | Mark the given constraint as insoluble. --- --- If the [W]anted constraint was made by 'newWantedWithProvenance', it will --- also mark the parent(s) from which the constraint was derived as insoluble. --- Even if they were previously assumed to be solved. -failWithProvenace :: Ct -> TcPluginM TcPluginResult -failWithProvenace ct = return (TcPluginContradiction (ct : parents)) - where - loc = ctLoc ct - lclbndrs = mapMaybe (\case {TcIdBndr id_ NotTopLevel -> Just id_ - ;_ -> Nothing }) - $ tcl_bndrs (ctLocEnv loc) - eqBndrs = filter ((\x -> case x of { EqPred NomEq _ _ -> True - ; _ -> False }) - . classifyPredType . snd) - $ map (\ev -> (ev,varType ev)) lclbndrs - parents = map (\(id_,p) -> mkNonCanonical $ CtWanted p id_ loc) eqBndrs -#endif - --- | Find a module -lookupModule :: ModuleName -- ^ Name of the module - -> FastString -- ^ Name of the package containing the module. - -- NOTE: This value is ignored on ghc>=8.0. - -> TcPluginM Module -lookupModule mod_nm _pkg = do -#if __GLASGOW_HASKELL__ >= 711 - hsc_env <- TcPluginM.getTopEnv - found_module <- TcPluginM.tcPluginIO $ Finder.findPluginModule hsc_env mod_nm -#else - found_module <- findImportedModule mod_nm $ Just _pkg -#endif - case found_module of -#if __GLASGOW_HASKELL__ >= 711 - FoundModule h -> return (fr_mod h) -#else - Found _ md -> return md -#endif - _ -> do - found_module' <- TcPluginM.findImportedModule mod_nm $ Just $ fsLit "this" - case found_module' of -#if __GLASGOW_HASKELL__ >= 711 - FoundModule h -> return (fr_mod h) -#else - Found _ md -> return md -#endif - _ -> panicDoc "Unable to resolve module looked up by plugin: " - (ppr mod_nm) - --- | Find a 'Name' in a 'Module' given an 'OccName' -lookupName :: Module -> OccName -> TcPluginM Name -lookupName md occ = lookupOrig md occ - --- | Print out extra information about the initialisation, stop, and every run --- of the plugin when @-ddump-tc-trace@ is enabled. -tracePlugin :: String -> TcPlugin -> TcPlugin -tracePlugin s TcPlugin{..} = TcPlugin { tcPluginInit = traceInit - , tcPluginSolve = traceSolve - , tcPluginStop = traceStop - } - where - traceInit = do - -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301 - initializeStaticFlags - tcPluginTrace ("tcPluginInit " ++ s) empty >> tcPluginInit - - traceStop z = tcPluginTrace ("tcPluginStop " ++ s) empty >> tcPluginStop z - - traceSolve z given derived wanted = do - tcPluginTrace ("tcPluginSolve start " ++ s) - (text "given =" <+> ppr given - $$ text "derived =" <+> ppr derived - $$ text "wanted =" <+> ppr wanted) - r <- tcPluginSolve z given derived wanted - case r of - TcPluginOk solved new -> tcPluginTrace ("tcPluginSolve ok " ++ s) - (text "solved =" <+> ppr solved - $$ text "new =" <+> ppr new) - TcPluginContradiction bad -> tcPluginTrace - ("tcPluginSolve contradiction " ++ s) - (text "bad =" <+> ppr bad) - return r - --- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301 -initializeStaticFlags :: TcPluginM () -#if __GLASGOW_HASKELL__ < 802 -initializeStaticFlags = tcPluginIO $ do - r <- readIORef v_opt_C_ready - unless r initStaticOpts -#else -initializeStaticFlags = return () -#endif - -#if __GLASGOW_HASKELL__ >= 804 --- | Flattens evidence of constraints by substituting each others equalities. --- --- __NB:__ Should only be used on /[G]iven/ constraints! --- --- __NB:__ Doesn't flatten under binders --- --- __NB:__ Only available on GHC 8.4+ -flattenGivens - :: [Ct] - -> [Ct] -flattenGivens givens = - mapMaybe flatToCt flat ++ map (substCt subst') givens - where - subst = mkSubst' givens - (flat,subst') - = second (map fst . concat) - $ partition ((>= 2) . length) - $ groupBy ((==) `on` (fst.fst)) - $ sortOn (fst.fst) subst - - flatToCt [((_,lhs),ct),((_,rhs),_)] - = Just - $ mkNonCanonical - $ CtGiven (mkPrimEqPred lhs rhs) (ctEvId ct) (ctLoc ct) - - flatToCt _ = Nothing - - --- | Create flattened substitutions from type equalities, i.e. the substitutions --- have been applied to each others right hand sides. --- --- __NB:__ Only available on GHC 8.4+ -mkSubst' :: [Ct] -> [((TcTyVar,TcType),Ct)] -mkSubst' = foldr substSubst [] . mapMaybe mkSubst - where - substSubst :: ((TcTyVar,TcType),Ct) - -> [((TcTyVar,TcType),Ct)] - -> [((TcTyVar,TcType),Ct)] - substSubst ((tv,t),ct) s = ((tv,substType (map fst s) t),ct) - : map (first (second (substType [(tv,t)]))) s - --- | Create simple substitution from type equalities --- --- __NB:__ Only available on GHC 8.4+ -mkSubst - :: Ct - -> Maybe ((TcTyVar, TcType),Ct) -mkSubst ct@(CTyEqCan {..}) = Just ((cc_tyvar,cc_rhs),ct) -mkSubst ct@(CFunEqCan {..}) = Just ((cc_fsk,TyConApp cc_fun cc_tyargs),ct) -mkSubst _ = Nothing - --- | Apply substitution in the evidence of Cts --- --- __NB:__ Only available on GHC 8.4+ -substCt - :: [(TcTyVar, TcType)] - -> Ct - -> Ct -substCt subst ct = - ct { cc_ev = (cc_ev ct) {ctev_pred = substType subst (ctev_pred (cc_ev ct))} - } - --- | Apply substitutions in Types --- --- __NB:__ Doesn't substitute under binders --- --- __NB:__ Only available on GHC 8.4+ -substType - :: [(TcTyVar, TcType)] - -> TcType - -> TcType -substType subst tv@(TyVarTy v) = case lookup v subst of - Just t -> t - Nothing -> tv -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 -#if __GLASGOW_HASKELL__ >= 809 -substType subst (FunTy af t1 t2) = - FunTy af (substType subst t1) (substType subst t2) -#else -substType subst (FunTy t1 t2) = - FunTy (substType subst t1) (substType subst t2) -#endif -substType _ l@(LitTy _) = l -substType subst (CastTy ty co) = - CastTy (substType subst ty) co -substType _ co@(CoercionTy _) = co -#endif +import Internal