Greetings, I'm working on improving the valid substitution feature that I implemented a few weeks ago, but I'm having a problem making it work with subsumption, i.e. if the types are not exactly equal. You can find all the code on a branch on my fork of GHC on GitHub https://github.com/Tritlo/ghc/tree/show-valid-substitutions-subsumes, with the subsumption checker being the following function: -- Reports whether one type subsumes another, discarding any errors tcSubsumes :: TcSigmaType -> TcSigmaType -> TcM Bool tcSubsumes hole_ty ty = discardErrs $ do { (_, wanted, _) <- pushLevelAndCaptureConstraints $ tcSubType_NC ExprSigCtxt ty hole_ty ; (rem, _) <- runTcS (simpl_top wanted) ; return (isEmptyWC rem) } The current example I'm working with is module T3 where ps3 :: Num a => a -> a -> a ps3 = (+) ps4 :: Num a => a -> a -> a ps4 = _ Which should of course include (+) as a suggestion. However, when it checks for (+), it does not report it as a match. What could be going wrong here? Could someone more familiar with the underlying machinery give some guidance on what could be going wrong here? Dumping the traceTc (i.e. running ./inplace/bin/ghc-stage2 -o test t3.hs -ddump-tc-trace) gives the following relevant output in the dump: Checking for substitution + parent:Num imported from ‘Prelude’ at t3.hs:1:8-9 (and originally defined in ‘GHC.Num’) tcSubType_NC an expression type signature forall a. Num a => a -> a -> a a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] tc_sub_tc_type (general case) ty_actual = forall a. Num a => a -> a -> a ty_expected = a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] tcSkolemise tc_sub_type_ds ty_actual = forall a. Num a => a -> a -> a ty_expected = a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] instCallConstraints [$dNum_a4eI] Instantiating all tyvars? True origin arising from a type equality forall a. Num a => a -> a -> a ~ a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] type forall a. Num a => a -> a -> a theta [Num a_a19t] leave_bndrs [] with [a_a4eH[tau:3]] theta: [Num a0_a4eH[tau:3]] tc_sub_type_ds ty_actual = a0_a4eH[tau:3] -> a0_a4eH[tau:3] -> a0_a4eH[tau:3] ty_expected = a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] tc_sub_type_ds ty_actual = a0_a4eH[tau:3] -> a0_a4eH[tau:3] ty_expected = a_a1D1[sk:2] -> a_a1D1[sk:2] tc_sub_type_ds ty_actual = a0_a4eH[tau:3] ty_expected = a_a1D1[sk:2] u_tys tclvl 3 a0_a4eH[tau:3] ~ a_a1D1[sk:2] arising from a type equality a0_a4eH[tau:3] -> a0_a4eH[tau:3] -> a0_a4eH[tau:3] ~ a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] u_tys tclvl 3 * ~ * arising from a kind equality arising from a0_a4eH[tau:3] ~ a_a1D1[sk:2] u_tys tclvl 3 'GHC.Types.LiftedRep ~ 'GHC.Types.LiftedRep arising from a kind equality arising from a0_a4eH[tau:3] ~ a_a1D1[sk:2] u_tys yields no coercion u_tys yields no coercion writeMetaTyVar a_a4eH[tau:3] :: * := a_a1D1[sk:2] u_tys yields no coercion tc_sub_tc_type (general case) ty_actual = a_a1D1[sk:2] ty_expected = a0_a4eH[tau:3] tcSkolemise tc_sub_type_ds ty_actual = a_a1D1[sk:2] ty_expected = a0_a4eH[tau:3] u_tys tclvl 3 a_a1D1[sk:2] ~ a0_a4eH[tau:3] arising from a type equality a0_a4eH[tau:3] -> a0_a4eH[tau:3] -> a0_a4eH[tau:3] ~ a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] u_tys yields no coercion tc_sub_tc_type (general case) ty_actual = a_a1D1[sk:2] ty_expected = a0_a4eH[tau:3] tcSkolemise tc_sub_type_ds ty_actual = a_a1D1[sk:2] ty_expected = a0_a4eH[tau:3] u_tys tclvl 3 a_a1D1[sk:2] ~ a0_a4eH[tau:3] arising from a type equality a0_a4eH[tau:3] -> a0_a4eH[tau:3] -> a0_a4eH[tau:3] ~ a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] u_tys yields no coercion newTcEvBinds unique = a4eJ solveWanteds { WC {wc_simple = [WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] (CNonCanonical)} solveSimpleWanteds { {[WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] (CNonCanonical)} ----------------------------- Start solver pipeline { work item = [WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] (CNonCanonical) inerts = {Unsolved goals = 0} rest of worklist = WL {} runStage canonicalization { workitem = [WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] (CNonCanonical) canonicalize (non-canonical) [WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] (CNonCanonical) canEvNC:cls Num [a0_a4eH[tau:3]] flatten_many { a0_a4eH[tau:3] Following filled tyvar a_a4eH[tau:3] = a_a1D1[sk:2] Unfilled tyvar a_a1D1[sk:2] flatten } a_a1D1[sk:2] canClass [WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] Num a_a1D1[sk:2] ContinueWith [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] end stage canonicalization } runStage interact with inerts { workitem = [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan) end stage interact with inerts } runStage top-level reactions { workitem = [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan) doTopReact [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan) matchClassInst pred = Num a_a1D1[sk:2] { matchClass not matching dict Num a_a1D1[sk:2] } matchClassInst result NoInstance try_fundeps [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan) end stage top-level reactions } insertInertCan { Trying to insert new non-eq inert item: [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan) addInertCan } Step 1[l:2,d:0] Kept as inert: [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] End solver pipeline (kept as inert) } final_item = [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan) getUnsolvedInerts tv eqs = {} fun eqs = {} insols = {} others = {[WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)} implics = {} Unflattening {Funeqs = Tv eqs =} Unflattening 1 {} Unflattening 2 {} Unflattening 3 {} Unflattening done {} zonkSimples done: {} solveSimpleWanteds end } iterations = 1 residual = WC {wc_simple = [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)} expandSuperClasses { End expandSuperClasses no-op } solveWanteds middle simples1 = {[WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)} simples2 = {[WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)} solveWanteds } final wc = WC {wc_simple = [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)} current evbinds = {} zonkSimples done: {[WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan(psc))} zonkSimples done: {} applyDefaultingRules { wanteds = WC {wc_simple = [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan(psc))} groups = [] info = ([Integer, Double], (False, False)) applyDefaultingRules } [] Constraint solver steps = 1 -- Matthías Páll Gissurarson