diff --git a/package.yaml b/package.yaml index c8e6337..7eccbb0 100644 --- a/package.yaml +++ b/package.yaml @@ -81,6 +81,7 @@ library: - hashable - deepseq - bytestring + - syb tests: pantomime-test: diff --git a/pantomime.cabal b/pantomime.cabal index 3f92e5e..d4eaf71 100644 --- a/pantomime.cabal +++ b/pantomime.cabal @@ -106,6 +106,7 @@ library , microlens , mtl , primitive + , syb , template-haskell , text , transformers diff --git a/src/Pantomime.hs b/src/Pantomime.hs index e2f1172..29ea468 100644 --- a/src/Pantomime.hs +++ b/src/Pantomime.hs @@ -4,7 +4,7 @@ module Pantomime ( plugin , Theory (..) - , PluginAxioms (..) + , Embeddings (..) , pantomime , pantomimeMarker , pantomimeNothing diff --git a/src/Pantomime/Annotation.hs b/src/Pantomime/Annotation.hs index f2a725f..5f85769 100644 --- a/src/Pantomime/Annotation.hs +++ b/src/Pantomime/Annotation.hs @@ -6,13 +6,13 @@ module Pantomime.Annotation ) where import Data.Data (Data) -import Pantomime.Axiom (PluginAxioms) +import Pantomime.Axiom (Embeddings) import GHC.Utils.Outputable (Outputable (..), hang) -- TODO: Not sure I like the name. This checks whether an expression whose -- result is of type Bool is valid. That is, whether it will always return True. data Theory where - Theory :: PluginAxioms -> Theory + Theory :: Embeddings -> Theory deriving (Show, Data) instance Outputable Theory where diff --git a/src/Pantomime/Axiom.hs b/src/Pantomime/Axiom.hs index 79c04e5..a63cb47 100644 --- a/src/Pantomime/Axiom.hs +++ b/src/Pantomime/Axiom.hs @@ -1,19 +1,29 @@ {-# LANGUAGE OverloadedStrings #-} +-- TODO: We should probably rename this module to 'Embed' at some point, but the +-- name is already taken by another module. Otherwise, 'Embedding' works. We'll +-- phase 'Embed' out likely at some point though, so maybe we can switch then. module Pantomime.Axiom - ( PluginAxioms (..) - , PluginAxiomsR (..) - , TypeAxiomsR - , TermAxiomsR - , resolvePluginAxioms + ( Embeddings (..) + , EmbeddingsR (..) + , TypeEmbeddingsR + , TermEmbeddingsR + , resolveEmbeddings ) where import Prelude hiding (break) import Language.Haskell.TH qualified as TH -import GHC.Core.TyCo.Rep (UnivCoProvenance(..)) -import GHC.Core.TyCon.Env (TyConEnv, mkTyConEnv) -import GHC.Data.TrieMap (TrieMap (..), insertTM) +import GHC.Core.InstEnv + ( InstEnvs (..) + , InstEnv + , mkLocalClsInst + , emptyInstEnv + , extendInstEnv + , unionInstEnv + ) +import GHC.Core.TyCo.Rep (UnivCoProvenance (..)) +import GHC.Core.Unfold.Make (mkDFunUnfolding) import GHC.Plugins ( TyCon (..) , Name @@ -23,56 +33,68 @@ import GHC.Plugins , Role (..) , Expr (..) , Var (..) - , TypeOrConstraint (..) + , Type + , MonadUnique (..) + , OverlapFlag (..) + , OverlapMode (..) , mkTyConTy , mkUnivCo , dataConWorkId , mkApps - , mkCast - , mkSymCo - , exprType + , mkAppTys + , mkTyVarTy + , mkVarOccFS + , mkGReflRightCo + , mkCastTy , classDataCon , typeKind - , unitExpr - , unrestricted - , emptyInScopeSet - , sORTKind_maybe , coercibleDataCon + , generatedSrcSpan + , setIdUnfolding + , isTypeSynonymTyCon + , expandTypeSynonyms + , splitTyConAppNoView_maybe + , unitDataConId ) -import GHC.Tc.Utils.TcType (eqType) +import GHC.Types.Id.Make (mkDictFunId) +import GHC.Types.Name (mkInternalName) import GHC.Utils.Outputable ( Outputable (..) , IsDoc (..) - , IsLine (fsep, (<+>), text) + , IsLine (fsep, (<+>), text, hcat) + , SDoc , hang , punctuate , comma , brackets ) +import GHC.Types.SourceText (SourceText(..)) -import GHC.Exts (IsList (..)) - -import Control.Monad ((>=>), guard, when) -import Control.Applicative (Alternative (..)) +import Control.Monad ((>=>)) import Data.Data (Data) -import Data.Function (on) -import Data.Map (Map) +import Data.Generics.Aliases (mkQ) +import Data.Generics.Schemes (something) import Data.Traversable (for) import Effectful +import Effectful.Context import Effectful.Error.Static +import Effectful.GHC.External (HasInstEnvs, getInstEnvs) import Effectful.GHC.TH import Effectful.GHC.TyThing -import Effectful.Context +import Effectful.GHC.Unique (HasUnique) -import Pantomime.BuiltIn (Embeddable) +import Pantomime.BuiltIn (Embeddable, Embedding (..)) import Pantomime.Unification (subsumeExpr) -import Pantomime.Util (foldM', freshId, foldlBy) +import Pantomime.Util (foldM') --- TODO: We're switching away from using 'Coercible' as it requires same runtime +-- TODO: This should be renamed to 'Embeddings' instead of 'Axioms'. We can +-- probably drop the 'Plugin' portion as well. -- kinded types: something we don't care about within the evaluator. Instead, -- we provide a custom typeclass. The comments should mirror this! +-- TODO: The text below should be updated to reflect the current state of +-- embeddings. We should at some point link the paper also. -- | User axioms only visible to the plugin. -- -- The kinds and types of the mapped terms should match up exactly. The @@ -112,15 +134,13 @@ import Pantomime.Util (foldM', freshId, foldlBy) -- 'BitVec'. The importance lies in using a coercion 'Coercible IntN BitVec'. -- -- > plusInterp --- > :: Coercible IntN BitVec +-- > :: Embeddable bv BitVec -- > => KnownNat n --- > => IntN n --- > -> IntN n --- > -> IntN n --- > plusInterp = go --- > where --- > go :: bv ~ BitVec => bv n -> bv n -> bv n --- > go = coerce plusIntN +-- > => bv n +-- > -> bv n +-- > -> bv n +-- > plusInterp = case embedding @bv @BitVec of +-- > Embedding -> coerce SMT.bvadd -- -- Note, the where clause is only to trick Haskell into allowing the coercion -- to appear at the top level. With this defintion in place, we supply the @@ -132,20 +152,24 @@ import Pantomime.Util (foldM', freshId, foldlBy) -- one-to-one. That is, to complete the interpretation, we supply 'plusInterp' -- with the user-supplied coercion that 'Coercible IntN BitVec'. Afterwards, the -- types match up and the function is a valid interpretation. -data PluginAxioms where - PluginAxioms :: - { typeAxioms :: Map TH.Name TH.Name - -- ^ Type-level representational equivalence axioms. +data Embeddings where + Embeddings :: + -- TODO: Probably want to remove the comment about fresh symbolic values + -- once we change the interface on this. + { typeEmbeddings :: [(TH.Name, TH.Name)] + -- ^ Type-level embeddings. -- - -- Both the key and value of these mappings should be resolvable to 'TyCon'. - -- One may think about this as providing an instance 'Coercible' to just the - -- plugin between the given 'TyCon'. This instance is used within the solver - -- when constructing fresh symbolic values and when resolving instances - -- for term-axioms. + -- Both the key and value of these mappings should be resolvable to a GHC + -- 'Type'. One may think about this as providing an instance 'Embeddable' + -- to the plugin between for the given types. This instance is used within + -- the solver when constructing fresh symbolic values and when resolving + -- instances for term-embeddings. -- TODO: Term axioms should allow for recursive definitions also. It -- probably won't be used much, but it would be good! I guess we would want -- a 'Bind' from GHC, but for template haskell names. - , termAxioms :: [(TH.Name, TH.Name)] + -- Actually, the above is not really required I think: the embedding can + -- always form a local recursive group. Will have to think about this! + , termEmbeddings :: [(TH.Name, TH.Name)] -- ^ Term-level representational equivalence axioms. -- -- Both the key and value of these mappings should be resolvable to 'Id'. @@ -157,68 +181,98 @@ data PluginAxioms where -- Note that this is a list because the ordering of the definitions does -- matter: any later definitions may use ones defined earlier. Duplicate -- definitions are considered an error. - } -> PluginAxioms + } -> Embeddings deriving (Show, Data) -instance Outputable PluginAxioms where - ppr PluginAxioms { .. } = do +instance Outputable Embeddings where + ppr Embeddings { .. } = do let pprKV (key, value) = text (show key) <+> ":->" <+> text (show value) let pprKVList pairs = brackets $ fsep $ punctuate comma $ pprKV <$> pairs - hang "PluginAxioms" 2 $ vcat - [ hang "Type Axioms:" 2 $ pprKVList (toList typeAxioms) - , hang "Term Axioms:" 2 $ pprKVList termAxioms + hang "Embeddings" 2 $ vcat + [ hang "Type Embeddings:" 2 $ pprKVList typeEmbeddings + , hang "Term Embeddings:" 2 $ pprKVList termEmbeddings ] -instance Semigroup PluginAxioms where - (<>) l r = PluginAxioms - { typeAxioms = typeAxioms l <> typeAxioms r - , termAxioms = termAxioms l <> termAxioms r +instance Semigroup Embeddings where + (<>) l r = Embeddings + { typeEmbeddings = typeEmbeddings l <> typeEmbeddings r + , termEmbeddings = termEmbeddings l <> termEmbeddings r } -instance Monoid PluginAxioms where - mempty = PluginAxioms - { typeAxioms = mempty - , termAxioms = mempty +instance Monoid Embeddings where + mempty = Embeddings + { typeEmbeddings = mempty + , termEmbeddings = mempty } -type TypeAxiomsR = TyConEnv TyCon +type TypeEmbeddingsR = InstEnv -- TODO: I guess these might be better suited as CoreBind no? -type TermAxiomsR = [(Id, CoreExpr)] +type TermEmbeddingsR = [(Id, CoreExpr)] -- TODO: I think it would be good to have type synonyms for both of these fields -- as we use them independently as well. -- | Fully resolved plugin axioms. These may be used as-is by the solver. -data PluginAxiomsR where - PluginAxiomsR :: - { typeAxiomsR :: TypeAxiomsR +data EmbeddingsR where + EmbeddingsR :: + { typeEmbeddingsR :: TypeEmbeddingsR -- ^ Type-level axioms, mainly used to construct symbolic values. - , termAxiomsR :: TermAxiomsR + , termEmbeddingsR :: TermEmbeddingsR -- ^ Term-level axioms, these already have their 'Coercible' instances -- resolved by the type-axioms, where applicable. -- -- This may be used to extend substitution environments. - } -> PluginAxiomsR - deriving (Data) + } -> EmbeddingsR -instance Outputable PluginAxiomsR where - ppr PluginAxiomsR { .. } = hang "PluginAxiomsR" 2 $ vcat - [ hang "Type Axioms:" 2 $ ppr typeAxiomsR - , hang "Term Axioms:" 2 $ ppr termAxiomsR +instance Outputable EmbeddingsR where + ppr EmbeddingsR { .. } = hang "EmbeddingsR" 2 $ vcat + [ hang "Type Embeddings:" 2 $ ppr typeEmbeddingsR + , hang "Term Embeddings:" 2 $ ppr termEmbeddingsR ] -instance Semigroup PluginAxiomsR where - (<>) l r = PluginAxiomsR - { typeAxiomsR = typeAxiomsR l <> typeAxiomsR r - , termAxiomsR = termAxiomsR l <> termAxiomsR r +instance Semigroup EmbeddingsR where + (<>) l r = EmbeddingsR + { typeEmbeddingsR = unionInstEnv (typeEmbeddingsR l) (typeEmbeddingsR r) + , termEmbeddingsR = termEmbeddingsR l <> termEmbeddingsR r } -instance Monoid PluginAxiomsR where - mempty = PluginAxiomsR - { typeAxiomsR = mempty - , termAxiomsR = mempty +instance Monoid EmbeddingsR where + mempty = EmbeddingsR + { typeEmbeddingsR = emptyInstEnv + , termEmbeddingsR = mempty } +-- TODO: I guess we should change this to 'isValidHeadArg' or something. Then +-- check if there are not any quantifiers or typeclass constraints in there, as +-- these are also disallowed! +-- | Finds a type synonym in a 'Type'. +hasSynonym :: Type -> Maybe TyCon +hasSynonym = something $ mkQ Nothing \ty -> do + case splitTyConAppNoView_maybe ty of + Just (tc, _) | isTypeSynonymTyCon tc -> Just tc + _ -> Nothing + +-- | Expand all type synonyms from a type. +-- +-- Throws an error if any type synonym still remains. +expandTypeSynonyms' + :: HasCallStack + => Error SDoc :> es + => Type + -> Eff es Type +expandTypeSynonyms' ty = do + let ty' = expandTypeSynonyms ty + case hasSynonym ty' of + Just tc -> throwError_ @SDoc $ hcat + [ "Type '" + , ppr ty' + , "' contains unsaturated type constructor '" + , ppr tc + , "' after type alias expansion." + ] + Nothing -> pure () + pure ty' + -- | Resolve user-supplied axioms in terms of Template Haskell names to their -- internal Core representation. -- @@ -233,181 +287,153 @@ instance Monoid PluginAxiomsR where -- Lastly, this also ensures that mappings are only made for OPAQUE functions. -- A special case here we do allow is a NOINLINE function without an unfolding. -- For these, we do not use any of the user-provided coercions. -resolvePluginAxioms +resolveEmbeddings :: HasCallStack - -- TODO: Adjust these errors! - => Error String :> es + -- TODO: Adjust the opaque SDoc error! + => Error SDoc :> es => Error (LookupError TH.Name) :> es => Error (LookupError Name) :> es => THNameToGHCName :> es => HasThings :> es + => HasUnique :> es + => HasInstEnvs :> es => Context Reader CoreProgram :> es => Context Reader [TyCon] :> es - => PluginAxioms - -> Eff es PluginAxiomsR -resolvePluginAxioms PluginAxioms { .. } = do + => Embeddings + -> Eff es EmbeddingsR +resolveEmbeddings Embeddings { .. } = do -- Get the typeclass we want to instantiate. - embedCls <- thNameToGhcName >=> lookupClass $ ''Embeddable - - -- Resolve the type-level axioms. This is simply a lookup for the TyCon. - typeAxiomsRList <- for (toList typeAxioms) \(orig, interp) -> do - let resolve = thNameToGhcName >=> lookupTyConAll - -- TODO: Should we ensure that the original TyCon is a data-type or newtype? - -- Otherwise, the conversion might be very fragile! Not sure if I'm missing - -- any here. - orig' <- resolve orig - interp' <- resolve interp - pure (orig', interp') - - -- Gather the dictionary map for instance resolution. - dicts <- foldM' emptyTM typeAxiomsRList \dicts (tcR, tcL) -> do - -- Gather the information to construct the coercion. - let prov = PluginProv "pantomime user-defined" - let tyL = mkTyConTy tcL - let tyR = mkTyConTy tcR - let co = mkUnivCo prov [] Representational tyL tyR - - -- Gather the dictionaries for 'Coercible'. - let dictCo = do - -- Get the kind of the coercible TyCon. - let kind = tyConKind tcL - - -- Ensure the kind and roles match up. - let eqKind = eqType kind $ tyConKind tcR - let eqRoles = all (uncurry (==)) $ on zip tyConRoles tcL tcR - guard $ eqKind && eqRoles - - -- Box the coercion. - let eqVar = Var $ dataConWorkId coercibleDataCon - let dictL = mkApps eqVar - [ Type kind - , Type tyL - , Type tyR - , Coercion co - ] - let dictR = mkApps eqVar - [ Type kind - , Type tyR - , Type tyL - , Coercion $ mkSymCo co - ] - pure (dictL, dictR) - - -- TODO: At some point I want to have 'Embeddable' to act like 'Coercible', - -- with the adjustment that we can also generate dictionaries here where - -- the final kind can differ. So to be precise, the kinds need to match up - -- precisely except the result kind. This one always has to be of kind - -- 'TYPE r' but the runtime representations do not have to match. - -- Gather the information to construct the final dictionary. - -- - -- Note that for all normal intents and purposes, 'Embeddable' should only - -- have instances when the kinds match up exactly. Only axioms may have - -- their representation differ, as these will never reach the runtime. - -- - -- At that point, we can also just evict the 'Coercible' instance that we - -- build up here. - -- Gather the dictionaries for 'Embeddable'. - let dictEm = do - -- Gather the RuntimeRep of the given types. - let runtimeRep ty = do - (sort, rty) <- sORTKind_maybe $ typeKind ty - case sort of - TypeLike -> pure rty - ConstraintLike -> empty - - repL <- runtimeRep tyL - repR <- runtimeRep tyR - let con = Var . dataConWorkId . classDataCon $ embedCls - -- TODO: For now, we're not really constructing the private typeclass - -- correctly. I don't think it's important for our use case, but it is - -- not very nice to do it like this. - let private = unitExpr - - -- Construct the embed function. - let (idE, _) = freshId "arg" (unrestricted tyL) emptyInScopeSet - let embed = Lam idE $ mkCast (Var idE) co - - -- Construct the project function. - let (idP, _) = freshId "arg" (unrestricted tyR) emptyInScopeSet - let project = Lam idP $ mkCast (Var idP) (mkSymCo co) - - -- Construct the typeclass dictionary. - pure $ mkApps con - [ Type repL - , Type repR - , Type tyL - , Type tyR - , private - , private - , embed - , project - ] - - -- Actually collect all dictionaries. - let dictCo' = maybe [] (\(l, r) -> [l, r]) dictCo - let dictEm' = maybe [] (: []) dictEm - let dictsNew = dictCo' <> dictEm' - - -- Throw an error if we could not create any. - when (null dictsNew) do - throwError @String "resolvePluginAxioms: could not create any Embeddable or Coercible dictionaries for the given axioms" - - -- Insert all dictionaries. - pure $ foldlBy dicts dictsNew \acc dict -> do - let ty = exprType dict - insertTM ty dict acc - - -- TODO: We should first ensure that termAxioms do not contain duplicate - -- definitions. + embeddable <- thNameToGhcName >=> lookupClass $ ''Embeddable + embedding <- thNameToGhcName >=> lookupDataCon $ 'Embedding + + -- Gather the instance environment for resolution. + typeEmbeddingsR <- foldM' emptyInstEnv typeEmbeddings \instEnv (tcL, tcR) -> do + let lookupTyConTH = thNameToGhcName >=> lookupTyConAll + tcL' <- lookupTyConTH tcL + tcR' <- lookupTyConTH tcR + + -- FIXME: We should ensure that the kinds for the type match up, up to + -- runtime representation. This latter part is hard though... + + -- TODO: There is a note in GHC that says the type variables in instance + -- declarations should be completely fresh. I don't think the type variables + -- on a TyCon are? If yes, this should be fine. If not, we should swap out + -- their 'Unique'. + -- Type variables that we will use in the instance declaration. + let tvs = case isTypeSynonymTyCon tcL' of + True -> tyConTyVars tcL' + False -> [] + + -- Apply the type variables to both type constructors and expand any type + -- synonyms. + let expand tc = do + let ty = mkAppTys (mkTyConTy tc) $ fmap mkTyVarTy tvs + -- TODO: Should we ensure that the expansion is actually only a + -- newtype or data declaration? I think yes. In fact, we should also + -- disallow quantifiers and typeclass requirements in this type! + expandTypeSynonyms' ty + tyL <- expand tcL' + tyR <- expand tcR' + + -- Construct the kind coercion used to create the 'Embedding' instance. + let prov = PluginProv "SymFC embedding (user-defined)" + let kindL = typeKind tyL + let kindR = typeKind tyR + let coK = mkUnivCo prov [] Nominal kindR kindL + + -- Use the coercion to make a version of the right-hand side that has the + -- same kind as the left-hand side. + let tyR' = mkCastTy tyR coK + + -- Construct the type coercion that will be exposed by `Coercible`. + let co = mkUnivCo prov [] Representational tyL tyR' + + -- Create the 'Coercible' dictionary. + let coercibleDict = mkApps (Var $ dataConWorkId coercibleDataCon) + [ Type kindL + , Type tyL + , Type tyR' + , Coercion co + ] + + -- Create the 'Embedding' data type. + let embed = mkApps (Var $ dataConWorkId embedding) + [ Type kindL + , Type kindR + , Type tyL + , Type tyR + , Type tyR' + , Coercion coK + , Coercion $ mkGReflRightCo Nominal tyR coK + , coercibleDict + ] + + -- The 'Embeddable' typeclass has a 'PrivateEmbeddable' requirement that is + -- there just so users cannot create an instance manually. It is essentially + -- a unit value with a different type, so we just pass in a unit as it is + -- never used. Slightly hacky, but it works (we cannot create the instance + -- correctly as it is not exported). + let private = Var unitDataConId + + -- Create the 'DFunUnfolding'. + let bndrs = [] + let dc = classDataCon embeddable + let args = [Type kindL, Type kindR, Type tyL, Type tyR, private, embed] + let unfolding = mkDFunUnfolding bndrs dc args + + -- Create a unique name for the embedding. + unique <- getUniqueM + let occ = mkVarOccFS "embedding" + let name = mkInternalName unique occ generatedSrcSpan + + -- Construct the initial 'DFunId', without unfolding. + let theta = [] -- No typeclass requirements in embeddings + let tys = [kindL, kindR, tyL, tyR] + let dfun = mkDictFunId name tvs theta embeddable tys + + -- Set the unfolding of the 'DFunId'. + let dfun' = setIdUnfolding dfun unfolding + + -- Create the local typeclass instance. + let overlap = OverlapFlag + { overlapMode = NoOverlap NoSourceText + , isSafeOverlap = False + } + let warn = Nothing + let inst = mkLocalClsInst dfun' overlap tvs embeddable tys warn + + -- TODO: We should check whether the functional dependency is being upheld. + -- We can do so with the function 'checkFundeps' from + -- 'GHC.Tc.Instance.FunDeps' + + -- Extend the instance environment with the embedding. + pure $ extendInstEnv instEnv inst + + -- Construct the instance environment used for subsumption. + instEnvs <- getInstEnvs + let instEnvs' = instEnvs + { ie_local = unionInstEnv typeEmbeddingsR $ ie_local instEnvs + } + + -- TODO: We should ensure that type embeddings and termAxioms do not + -- contain duplicate definitions. -- Gather a binder mapping for a substitution. This will use the dictionary -- map to supply coercions to any Opaque values that require it. - termAxiomsR <- for termAxioms \(orig, interp) -> do + termEmbeddingsR <- for termEmbeddings \(orig, interp) -> do -- Resolve the names as identifiers. - let resolve = thNameToGhcName >=> lookupIdAll - orig' <- resolve orig - interp' <- resolve interp - - -- TODO: I'm not sure what to do with this. Should we just always resolve - -- using the embeddings? - -- -- Gather the expression of the interpretation. - -- -- TODO: Should we also attempt to get it from the local bindings? - -- expr <- case realIdUnfolding interp' of - -- CoreUnfolding { uf_tmpl } -> pure uf_tmpl - -- _ -> throwError_ () - - -- -- Check whether the original target can be interpreted. - -- dicts' <- case inl_inline $ idInlinePragma orig' of - -- -- Opaque values can be fully interpreted. Hence, we resolve any coercions - -- -- that were provided by the user. - -- Opaque _ -> pure dicts - - -- -- We only want to interpret no-inline if the unfolding was not available. - -- NoInline _ | not . hasCoreUnfolding $ realIdUnfolding orig' -> do - -- pure emptyTM - - -- -- It is fragile to interpret inlineable instances, as they may already - -- -- have been optimised away. - -- -- FIXME: It seems that the 'noinline' function has a NOINLINE pragma - -- -- but when testing it here, it doesn't. I feel like this test is the - -- -- correct one but it doesn't work in this case. I'll leave it like this - -- -- for now. - -- -- - -- -- Actually, I ran into an issue where the function I wanted to call had - -- -- a NOINLINE on an inner value (that was not exported). Perhaps it still - -- -- makes sense to overwrite definitions, even if they can be inlined? I - -- -- guess it is still pretty fragile... - -- -- _ -> throwError_ () - -- _ -> pure emptyTM + let lookupIdTH = thNameToGhcName >=> lookupIdAll + orig' <- lookupIdTH orig + interp' <- lookupIdTH interp -- Check whether the interpretation matches. - expr' <- subsumeExpr dicts (Var interp') $ varType orig' + expr' <- subsumeExpr instEnvs' (Var interp') $ varType orig' -- Return the mapping. pure (orig', expr') -- Collect the resolved type and term mappings. - pure PluginAxiomsR - { typeAxiomsR = mkTyConEnv typeAxiomsRList - , termAxiomsR + pure EmbeddingsR + { typeEmbeddingsR + , termEmbeddingsR } diff --git a/src/Pantomime/Binding.hs b/src/Pantomime/Binding.hs index e4ad7e7..a4c28ac 100644 --- a/src/Pantomime/Binding.hs +++ b/src/Pantomime/Binding.hs @@ -14,7 +14,7 @@ import Control.Monad ((>=>)) import Data.Traversable (for) import Effectful import Effectful.Error.Static -import Effectful.GHC.TyThing (HasThings, lookupTyCon, lookupId) +import Effectful.GHC.TyThing (HasThings, lookupTyCon, lookupId, lookupClass) import Effectful.GHC.TH (THNameToGHCName, thNameToGhcName) import GHC.Plugins (Name, Var, Id) import GHC.TypeNats qualified as Builtin (type (<=)) @@ -100,6 +100,7 @@ getBuiltinTyCon = do tcKnownNat <- thNameToTyCon ''Builtin.KnownNat tcLEqNat <- thNameToTyCon ''(Builtin.<=) tcUnsafeEquality <- thNameToTyCon ''Builtin.UnsafeEquality + clsEmbeddable <- (thNameToGhcName >=> lookupClass) ''Builtin.Embeddable pure BuiltInTyCon { .. } bindingsTH :: [(TH.Name, forall es. PrimOp es)] diff --git a/src/Pantomime/BuiltIn.hs b/src/Pantomime/BuiltIn.hs index cb2e43d..c4acc04 100644 --- a/src/Pantomime/BuiltIn.hs +++ b/src/Pantomime/BuiltIn.hs @@ -1,4 +1,5 @@ {-# LANGUAGE BangPatterns #-} +{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} @@ -21,7 +22,9 @@ -- you're doing! module Pantomime.BuiltIn -- | Embeddable constraint for user interpretations. - ( Embeddable (..) + ( Embeddable + , Embedding (..) + , embedding -- | Typeclass to differentiate primitive types. , Primitive (..) @@ -174,7 +177,7 @@ module Pantomime.BuiltIn import Control.Monad.Identity (Identity (..)) import Data.Bits qualified as Prelude (Bits (..)) -import Data.Coerce (coerce) +import Data.Coerce (Coercible, coerce) import Data.Constraint (Dict (..), HasDict (..)) import Data.Constraint.Unsafe qualified as Prelude (unsafeSNat) import Data.Composition ((.:)) @@ -218,7 +221,7 @@ import GHC.Word , Word64 (..) ) import Grisette - ( SymShift(..) + ( SymShift (..) , SizedBV (..) , SignConversion (..) , BitCast (..) @@ -230,28 +233,75 @@ import Pantomime.Util qualified as Util (BitVec, (%+)) import Prelude qualified import Prelude (Applicative (..), Ordering (..), Maybe (..), ($), (.)) --- TODO: I guess we could also make this a typeclass without variables? -class Private a - -instance Private a - --- TODO: At some point I want this typeclass to have behaviour like 'Coercible'. --- For now, I'll leave it like this as it eases the implementation quite a bit. -class (Private a, Private b) => Embeddable (a :: TYPE r1) (b :: TYPE r2) where - embed :: a -> b - project :: b -> a - --- class Private a b => Embeddable (a :: k1) (b :: k2) - +-- Below some stubs if we ever want to make 'Embeddable' be like 'Coercible' +-- without the evidence pattern matching. +-- +-- If we do go full 'Embeddable' route with a typechecker plugin: we likely want +-- to call 'solveEquality' from 'GHC.Tc.Solver.Equality' with the given +-- constraints that all runtime representations are nominally equivalent. +-- +-- class PrivateEmbeddable => Embeddable (a :: k1) (b :: k2) +-- -- embed -- :: forall {r1} {r2} (a :: TYPE r1) (b :: TYPE r2) -- . Embeddable a b -- => a -- -> b --- embed = embed +-- embed = noinline embed + +-- | Unexported typeclass that has no instances. +-- +-- This disallows any instance of 'Embeddable' to be defined as this typeclass +-- requirement is not exported *and* does not have an instance. +class PrivateEmbeddable + +-- | Evidence of a 'Coercible' instance for different kinded types. +-- +-- Example embedding of a type to a 64-bit sized bit vector. The evidence +-- provided by 'Embeddable' is generated by the symbolic evaluator via type +-- embeddings. Term embeddings can consume these instances of 'Embeddable'. +-- +-- ``` +-- plus64 :: forall {r} (a :: TYPE r). Embeddable a (BitVec 64) => a -> a -> a +-- plus64 = case embedding of Embedding -> coerce bvadd +-- ``` +-- +-- Note that only the plugin can safely generate heterogenous coercions. They +-- are only safe under symbolic evaluation given a coherent set of embeddings. +-- +-- Of course, a user is free to construct an instance for a homogenous coercion. +-- +-- Unlike 'Coercible', 'Embeddable' is not symmetric. The first type argument is +-- the source type (i.e. the type to embed) and the second type argument is the +-- destination type (i.e. the interpretation). +class PrivateEmbeddable => Embeddable (a :: k1) (b :: k2) | a -> b where + -- | Get the 'Embedding' instance of the typeclass. + -- + -- We expose 'embedding' as it keeps the kind arguments invisible, which is + -- more ergonomic. + embedding' :: Embedding a b + +-- Instance to allow resolution of embeddings with more type saturation than +-- strictly required. +instance (PrivateEmbeddable, Embeddable a b) => Embeddable (a c) (b c) where + embedding' = case embedding @a of Embedding -> Embedding + +-- | Get the 'Embedding' instance of the typeclass. +embedding + :: forall {k1} {k2} (a :: k1) (b :: k2) + . Embeddable a b + => Embedding a b +embedding = embedding' + +-- | Data type carrying of a 'Coercible' instance for different kinded types. +-- +-- See 'Embeddable' for more information. +data Embedding (a :: k1) (b :: k2) where + Embedding :: Coercible a b => Embedding a b -- TODO: For now, we'll just have the platform sized as 64-bit. Not sure how -- we would handle this correctly? Maybe with a pragma? +-- | The bit size of this platforms 'Int#' and 'Word#' primitive. type PlatformWordSize = 64 -- | Literal construction function for built-in Haskell 'Int#' literal. diff --git a/src/Pantomime/Fresh.hs b/src/Pantomime/Fresh.hs index e5c5054..fc29da9 100644 --- a/src/Pantomime/Fresh.hs +++ b/src/Pantomime/Fresh.hs @@ -1,22 +1,22 @@ {-# LANGUAGE OverloadedStrings #-} module Pantomime.Fresh - ( FreshInstEnv (..) - , freshArgs + ( freshArgs ) where import GHC.Builtin.Types.Prim (eqPrimTyCon, eqReprPrimTyCon) -import GHC.Core.FamInstEnv (topReduceTyFamApp_maybe, FamInstEnvs) +import GHC.Core.FamInstEnv (FamInstEnvs, topReduceTyFamApp_maybe) +import GHC.Core.InstEnv (InstEnvs (..), unionInstEnv) import GHC.Core.Reduction (Reduction (..), mkReduction, homogeniseHetRedn) import GHC.Core.TyCo.Rep (scaledThing, UnivCoProvenance (..)) -import GHC.Core.TyCon.Env (TyConEnv, lookupTyConEnv) import GHC.Core.Unify (tcUnifyTysFG, alwaysBindFun, UnifyResultM (..)) -import GHC.Types.Unique (Uniquable (..), getKey) +import GHC.Data.Pair (Pair(..)) +import GHC.Tc.Instance.FunDeps (improveFromInstEnv, FunDepEqn (..)) +import GHC.Types.Unique (Uniquable (..), getKey, minLocalUnique, incrUnique) import GHC.Utils.Outputable (Outputable (..), text, (<+>), showSDocUnsafe) import GHC.Plugins qualified as GHC import GHC.Plugins ( Var - , TyCon , Name , DataCon , InScopeSet @@ -33,17 +33,17 @@ import GHC.Plugins , splitTyConApp_maybe , tyConFamilySize , tyVarKind - , mkTyConTy , mkUnivCo - , mkAppCos , mkReflCo , mkSymCo , mkSubCo + , mkTyConTy , coreFullView , coercionRKind , instNewTyCon_maybe , getOccFS , bytesFS + , tyConKind ) import Grisette @@ -62,11 +62,11 @@ import Data.Constraint (Dict (..)) import Data.Text.Encoding (decodeUtf8) import Data.Traversable (for) -import Pantomime.Axiom (TypeAxiomsR) +import Pantomime.Axiom (TypeEmbeddingsR) import Pantomime.Defer (Deferrable, defer) import Pantomime.Expr import Pantomime.Literal - ( BuiltInTyCon + ( BuiltInTyCon (..) , SomeLiteralType (..) , HasDict (..) , projectLitTy @@ -77,11 +77,6 @@ import Effectful import Effectful.Error.Static import Effectful.Context (Context, ContextMode (..), get) -data FreshInstEnv where - FreshInstEnv :: - { fieUser :: TyConEnv TyCon - } -> FreshInstEnv - data Variable where Variable :: { varName :: Name @@ -161,16 +156,22 @@ freshExpr => Deferrable es => Error String :> es => Context Reader FamInstEnvs :> es + => Context Reader InstEnvs :> es => Context Reader BuiltInTyCon :> es - => TyConEnv TyCon + => TypeEmbeddingsR -> Var -> Eval es Expr -freshExpr axioms root = do +freshExpr embeddings root = do -- TODO: Is it better to this lookup once? Whilst it is a reader-like effect, -- it is implemented through IO, so I'm a bit wary of running it in a hot loop -- like this one. The only way to know is just to profile I guess, but for now -- I'll put it outside. fam <- liftEff $ get @FamInstEnvs + instEnvs <- liftEff $ get @InstEnvs + let instEnvs' = instEnvs + { ie_local = unionInstEnv embeddings $ ie_local instEnvs + } + BuiltInTyCon { clsEmbeddable } <- liftEff $ get @BuiltInTyCon -- TODO: Add note on callstack and recursion -- TODO: I don't like the nesting this gives. Maybe we should move these -- definitions inwards somehow. Perhaps just a standalone helper definition? @@ -218,17 +219,26 @@ freshExpr axioms root = do -- User Interpretation: ----------------------- - | Just (tc, args) <- splitTyConApp_maybe ty - , Just tc' <- lookupTyConEnv axioms tc -> do + | Just (tc, targs) <- splitTyConApp_maybe ty + + -- Construct a fresh type and kind variable. + , let namekv = GHC.mkSystemName minLocalUnique $ GHC.mkVarOccFS "k" + , let k = GHC.mkTyVarTy $ GHC.mkTyVar namekv GHC.liftedTypeKind + , let namea = GHC.mkSystemName (incrUnique minLocalUnique) $ GHC.mkVarOccFS "a" + , let a = GHC.mkTyVarTy $ GHC.mkTyVar namea k + + -- Lookup an instance using the functional dependency. + , let kind = tyConKind tc + , let args = [kind, k, mkTyConTy tc, a] + , let deps = improveFromInstEnv instEnvs' (const ()) clsEmbeddable args + , [FDEqn { fd_eqs = [Pair tyR _]}] <- deps -> do -- Construct the plugin coercion - let prov = PluginProv "pantomime user-defined" - let tyL = mkTyConTy tc - let tyR = mkTyConTy tc' - let univ = mkUnivCo prov [] Representational tyL tyR - let co = mkAppCos univ $ mkReflCo Nominal <$> args + let prov = PluginProv "SymFC embedding (user-defined)" + let co = mkUnivCo prov [] Representational (GHC.mkTyConTy tc) tyR + let co' = GHC.mkAppCos co $ mkReflCo Nominal <$> targs -- Create the final expression. - mkReductionCast $ mkReduction co (coercionRKind co) + mkReductionCast $ mkReduction co' (coercionRKind co') -- Type-Family: --------------- @@ -400,12 +410,13 @@ freshArgs => Error String :> es => Context Reader BuiltInTyCon :> es => Context Reader FamInstEnvs :> es - => TypeAxiomsR + => Context Reader InstEnvs :> es + => TypeEmbeddingsR -> [String] -> Type -> InScopeSet -> Eff es ([(Var, Arg)], InScopeSet) -freshArgs axioms valNames ty scope0 = do +freshArgs embeddings valNames ty scope0 = do -- Gather the argument types. let (tyVars, funTy) = splitForAllTyVars ty let (argTys, _resTy) = splitFunTys funTy @@ -425,7 +436,7 @@ freshArgs axioms valNames ty scope0 = do let args = tyArgs <> valArgs -- Create symbolic instance of the arguments. - symbolic <- for args $ defer . freshExpr axioms + symbolic <- for args $ defer . freshExpr embeddings -- Zip the binders together with their symbolic instance. let binders = zip args symbolic diff --git a/src/Pantomime/Literal.hs b/src/Pantomime/Literal.hs index d5d2f16..1d172e0 100644 --- a/src/Pantomime/Literal.hs +++ b/src/Pantomime/Literal.hs @@ -27,7 +27,7 @@ module Pantomime.Literal import Control.Applicative (Alternative(..)) import Control.Monad ((>=>)) -import Data.Constraint +import Data.Constraint (Dict (..), HasDict (..), withDict) import Data.Functor.Identity (Identity(..)) import Data.Maybe (isJust) import Data.Proxy (Proxy(..)) @@ -37,6 +37,7 @@ import Effectful import Effectful.Context import Effectful.Error.Static +import GHC.Core.Class (Class) import GHC.Core.Reduction (Reduction(..)) import GHC.Core.FamInstEnv (normaliseType, FamInstEnvs) import GHC.Plugins @@ -306,6 +307,7 @@ data BuiltInTyCon where , tcKnownNat :: TyCon , tcLEqNat :: TyCon , tcUnsafeEquality :: TyCon + , clsEmbeddable :: Class } -> BuiltInTyCon -- | Convert a 'LiteralType' into a Haskell 'Type'. diff --git a/src/Pantomime/Passes.hs b/src/Pantomime/Passes.hs index 58d47b7..51431e0 100644 --- a/src/Pantomime/Passes.hs +++ b/src/Pantomime/Passes.hs @@ -7,8 +7,6 @@ import GHC.Plugins hiding (empty, (<>), thNameToGhcName, getFirstAnnotations) import GHC.Core.Lint import GHC.Driver.Config.Core.Lint (initLintConfig) -import GHC.Core.Make (mkStringExpr) - import Grisette ( GrisetteSMTConfig (..) , SMTConfig (..) @@ -28,7 +26,7 @@ import Language.Haskell.TH qualified as TH import Pantomime.Solve import Pantomime.Unification -import Pantomime.Axiom (resolvePluginAxioms) +import Pantomime.Axiom (resolveEmbeddings) import Pantomime.Annotation import Effectful @@ -45,6 +43,7 @@ import Effectful.GHC.Display import Effectful.GHC.TyThing import Effectful.GHC.External import Effectful.GHC.Annotations +import Effectful.GHC.Unique (HasUnique) -- | An always non-recursive binder. data Bind' a = Bind' a (Expr a) @@ -106,12 +105,14 @@ runSymbolic , Error UnificationError , Error SolverError , Error String + , Error SDoc , Provider_ Solver () , HasAnnotations , THNameToGHCName , HasThings , Context Reader CoreProgram , Context Reader [TyCon] + , HasUnique , HasInstEnvs , HasFamInstEnvs , HasExternalPackageState @@ -130,12 +131,14 @@ runSymbolic guts . runHasExternalPackageState . runHasFamInstEnv guts . runHasInstEnvs guts + . runHasUnique . runContextReader (mg_tcs guts) . runContextReader (mg_binds guts) . runHasThings . runThNameToGhcName . runHasAnnotations . runProvider_ (const $ runSolver solver) + . runErrorWith @SDoc propagateError . runErrorWith @String propagateErrorShow . runErrorWith @SolverError propagateErrorShow . runErrorWith @UnificationError propagateError @@ -201,6 +204,7 @@ printAndLint bind = do checkValidityAndEmbed :: ( HasCallStack , Error String :> es + , Error SDoc :> es , Error (LookupError Name) :> es , Error (LookupError TH.Name) :> es , Error SolverError :> es @@ -208,12 +212,13 @@ checkValidityAndEmbed , Context Reader [TyCon] :> es , Provider_ Solver () :> es , HasFamInstEnvs :> es + , HasInstEnvs :> es , HasThings :> es + , HasUnique :> es , THNameToGHCName :> es , HasAnnotations :> es , CoreE :> es , IOE :> es - , HasDynFlagsE :> es ) => ModGuts -> Eff es ModGuts @@ -225,9 +230,9 @@ checkValidityAndEmbed guts = do justId <- thNameToGhcName 'pantomimeJust >>= lookupIdAll (binds, results) <- fmap unzip $ for (mg_binds guts) \case - NonRec x e | Just (Theory axioms) <- lookupUFM anns $ varName x -> do - axioms' <- resolvePluginAxioms axioms - mCounterexample <- checkValid axioms' e + NonRec x e | Just (Theory embeddings) <- lookupUFM anns $ varName x -> do + embeddings' <- resolveEmbeddings embeddings + mCounterexample <- checkValid embeddings' e let varNameStr = getOccString x case mCounterexample of Nothing -> do diff --git a/src/Pantomime/Solve.hs b/src/Pantomime/Solve.hs index a6c79f9..5672354 100644 --- a/src/Pantomime/Solve.hs +++ b/src/Pantomime/Solve.hs @@ -32,7 +32,6 @@ import GHC.Plugins , Bind (..) , Var , exprType - , varType , vcat , emptyInScopeSet , getOccString @@ -71,7 +70,7 @@ import Pantomime.Symbolise import Pantomime.Subst import Pantomime.Fresh import Pantomime.Util (dbg) -import Pantomime.Axiom (PluginAxiomsR (..)) +import Pantomime.Axiom (EmbeddingsR (..)) import Pantomime.PrimOps (PrimOp) import Pantomime.Defer (defer, withDeferrable) import Pantomime.Binding @@ -90,6 +89,7 @@ import Effectful.GHC.External import Effectful.Grisette.Solver import Effectful.Provider import Effectful.Exception (ErrorCall (..), throwIO) +import GHC.Core.InstEnv (InstEnvs) -- TODO: Definitely not the cleanest place to add these effects. I should look -- into where to do this. @@ -97,21 +97,24 @@ runBuiltInTypes :: Error (LookupError TH.Name) :> es => Error (LookupError Name) :> es => HasThings :> es - => THNameToGHCName :> es => HasFamInstEnvs :> es - => Eff (Context Reader BuiltInTyCon : Context Reader InterfaceThings : Context Reader FamInstEnvs : es) a + => HasInstEnvs :> es + => THNameToGHCName :> es + => Eff (Context Reader BuiltInTyCon : Context Reader InterfaceThings : Context Reader FamInstEnvs : Context Reader InstEnvs : es) a -> Eff es a runBuiltInTypes eff = do tys <- getBuiltinTyCon ids <- getInterfaceThings fam <- getFamInstEnvs - runContextReader fam . runContextReader ids . runContextReader tys $ eff + env <- getInstEnvs + runContextReader env . runContextReader fam . runContextReader ids . runContextReader tys $ eff type SymboliseEff = [ Context Reader BuiltInTyCon , Context Reader InterfaceThings , Context Reader FamInstEnvs , Error String + , Context Reader InstEnvs ] newtype Lie a where @@ -127,15 +130,16 @@ construct => Context Reader InterfaceThings :> es => Context Reader FamInstEnvs :> es => Error String :> es + => Context Reader InstEnvs :> es => [(Var, forall fs. PrimOp fs)] - -> PluginAxiomsR + -> EmbeddingsR -> CoreProgram -> CoreExpr -- FIXME: This 'Lie' evades the check NFData constraint on 'withDeferrable'. -- I'm not sure how to go around this, so for now we just let it crash if it -- does occur.. :/ -> Eff es (SymBool, Lie (Eff SymboliseEff [(Var, Arg)])) -construct prim PluginAxiomsR { .. } program expr = inject @SymboliseEff $ withDeferrable do +construct prim EmbeddingsR { .. } program expr = inject @SymboliseEff $ withDeferrable do prim' <- for prim \(bndr, rhs) -> do rhs' <- defer rhs pure (bndr, rhs') @@ -144,7 +148,7 @@ construct prim PluginAxiomsR { .. } program expr = inject @SymboliseEff $ withDe subst0 <- extendIdSubstMany mkEmptySubst prim' -- Add the term bindings to the substitution. - let termAxiomsR' = uncurry NonRec <$> termAxiomsR + let termAxiomsR' = uncurry NonRec <$> termEmbeddingsR subst1 <- symboliseBindMany subst0 termAxiomsR' -- TODO: I think there is an ordering problem here between user @@ -159,7 +163,7 @@ construct prim PluginAxiomsR { .. } program expr = inject @SymboliseEff $ withDe -- Create fresh arguments. let ty = exprType expr - (args, _scope) <- freshArgs typeAxiomsR (collectValBinders expr) ty emptyInScopeSet + (args, _scope) <- freshArgs typeEmbeddingsR (collectValBinders expr) ty emptyInScopeSet result <- defer do fun <- symbolise subst expr @@ -203,11 +207,12 @@ checkValid => Error (LookupError Name) :> es => Error SolverError :> es => Context Reader CoreProgram :> es + => HasInstEnvs :> es => HasThings :> es => THNameToGHCName :> es => HasFamInstEnvs :> es => Provider_ Solver () :> es - => PluginAxiomsR + => EmbeddingsR -> CoreExpr -> Eff es (Maybe Counterexample) checkValid axioms expr = runBuiltInTypes do @@ -219,7 +224,7 @@ checkValid axioms expr = runBuiltInTypes do -- TODO: Is there perhaps a better place to add this? Ideally we just do it -- as a normal axiom, but I cannot find where 'nospec' is defined... idId <- thNameToGhcName 'id >>= lookupIdAll - let axioms' = axioms { termAxiomsR = (nospecId, GHC.Var idId) : termAxiomsR axioms } + let axioms' = axioms { termEmbeddingsR = (nospecId, GHC.Var idId) : termEmbeddingsR axioms } (eq, Lie args) <- construct prim axioms' program expr diff --git a/src/Pantomime/Unification.hs b/src/Pantomime/Unification.hs index 1462c3b..603ef12 100644 --- a/src/Pantomime/Unification.hs +++ b/src/Pantomime/Unification.hs @@ -4,16 +4,15 @@ -- naming from GHC. -- TODO: Add module docs. module Pantomime.Unification - ( UnificationError (..), - OversaturatedError (..), - unifyApp, - unifyApps, - unifyExprs, - resolveInstances, - resolveInstancesWith, - subsumeExpr, - ) -where + ( UnificationError (..) + , OversaturatedError (..) + , unifyApp + , unifyApps + , unifyExprs + , resolveInstances + , resolveInstancesWith + , subsumeExpr + ) where import Control.Applicative (Alternative ((<|>))) import Control.Error (LookupError (..)) @@ -26,7 +25,7 @@ import Effectful.Context import Effectful.Error.Static import Effectful.GHC.External (HasInstEnvs, lookupUniqueInst) import GHC.Core.Class (Class) -import GHC.Core.InstEnv (instanceDFunId) +import GHC.Core.InstEnv (InstEnvs, instanceDFunId, lookupUniqueInstEnv) import GHC.Core.Map.Type (TypeMap) import GHC.Core.Predicate (isEvVar) import GHC.Core.TyCo.Rep (Scaled (..), Type (..), scaledThing) @@ -34,7 +33,7 @@ import GHC.Core.Unify (alwaysBindFun, tcMatchTy, tcUnifyTys) import GHC.Data.Maybe (rightToMaybe, whenIsJust) import GHC.Data.TrieMap (TrieMap (..), insertTM) import GHC.Plugins hiding ((<>)) -import GHC.Tc.Utils.TcType (substTy, tcSplitSigmaTy) +import GHC.Tc.Utils.TcType (substTy, tcSplitSigmaTy, tcSplitDFunHead) import Lens.Micro import Lens.Micro.Extras (view) import Pantomime.Util @@ -387,42 +386,54 @@ unifyExprs lhs rhs = do -- TODO: Using 'TypeMap CoreExpr' for instances is extremely fragile. It would -- be a lot better to use InstEnv to resolve typeclasses. This goes for other -- functions in this module as well! -subsumeExpr :: - (HasCallStack) => - (Error String :> es) => - TypeMap CoreExpr -> - CoreExpr -> - Type -> - Eff es CoreExpr -subsumeExpr dicts expr ty = do +subsumeExpr + :: HasCallStack + => Error SDoc :> es + => InstEnvs + -> CoreExpr + -> Type + -> Eff es CoreExpr +subsumeExpr insts expr ty = do -- Get the unifiable part of the type. let (curTv, curEv, curTy) = splitExprTy expr let (reqTv, reqEv, reqTy) = tcSplitSigmaTy ty -- Match the types and add all dictionaries we care about. - let err = - "subsumeExpr: type matching failed" - <> "\n current type: " - <> showSDocUnsafe (ppr curTy) - <> "\n required type: " - <> showSDocUnsafe (ppr reqTy) - subst <- failWith err $ tcMatchTy curTy reqTy + let err = hcat + [ "Could not match '" + , ppr curTy + , "' to the required type '" + , ppr reqTy + , "'." + ] + subst <- failWith @SDoc err $ tcMatchTy curTy reqTy -- Make evidence variables. let names = ("dict",) . unrestricted <$> reqEv let (lamEv, _) = freshIds names $ mkInScopeSetList reqTv - -- Construct the arguments to supply to the expression to unify. + -- Construct the local arguments to supply to the expression to unify. let argsTv = substTy subst . mkTyVarTy <$> curTv - let dicts' = foldlBy dicts lamEv \acc ev -> do - insertTM (varType ev) (Var ev) acc + let dicts = foldlBy emptyTM lamEv \acc ev -> do + insertTM @TypeMap (varType ev) ev acc + + -- Get the required typeclasses. let curEv' = substTy subst <$> curEv - argsEv <- for curEv' \ev -> do - let err' = - "subsumeExpr: type variable instance not found in dictionary" - <> "\n type: " - <> showSDocUnsafe (ppr ev) - failWith @String err' $ lookupTM ev dicts' + argsEv <- for curEv' \ev -> runBreak do + -- First try to find a local instance that is supplied to the function. + whenIsJust (lookupTM ev dicts) $ break . Var @CoreBndr + + -- If no local instance exists, try to resolve the through the instance + -- environment. + let (cls, args) = tcSplitDFunHead ev + case lookupUniqueInstEnv insts cls args of + Right (inst, targs) -> pure $ mkTyApps (Var $ instanceDFunId inst) targs + -- TODO: Improve error message! + Left _err -> throwError_ @SDoc $ hcat + [ "Instance lookup of typeclass '" + , ppr ev + , "' failed when subsuming expression." + ] -- Construct the new expression. let open = mkApps expr $ fmap Type argsTv <> argsEv