L.S., I've come up with some minor progress myself, but I could still do with a little help. The attached file is the smallest thing I could come up with to replicate my problem. I'm using tcMatchTy now to try and match two types, hoping to find TyVar substitutions when the types unify. Given the functions in the attached file and the ghci-session below this message (from the current Haskell Platform), could anyone explain the misses (the ones that result in Nothing)?? Regards, Philip P.S. Note that type variables are pretty printed to simply 'a' or 'b'. The names are disambiguated only locally, so in the trace below, not every 'a' is equal to every other 'a' (but this becomes obvious from the corresponding InScopeSet) Ghci session: *CheckType> matchHole "fmap" 0 "id" Hole: FunTy (TyVarTy a) (TyVarTy b) Term: FunTy (TyVarTy a) (TyVarTy a) Vars: [a,b,a] Just (TvSubst InScopeSet [(a15M9,a),(a15Ma,b),(a15Mg,a)] [(a15M9,TyVarTy a),(a15Ma,TyVarTy a)]) *CheckType> matchHole "fmap" 0 "(+)" Hole: FunTy (TyVarTy a) (TyVarTy b) Term: FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (FunTy (TyVarTy a) (FunTy (TyVarTy a) (TyVarTy a))) Vars: [a,b,a] Nothing *CheckType> matchHole "(+)" 0 "0" Hole: FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (TyVarTy a) Term: FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (TyVarTy a) Vars: [a,a] Just (TvSubst InScopeSet [(a168l,a),(a168s,a)] [(a168l,TyVarTy a)]) *CheckType> matchHole "fmap" 1 "[True]" Hole: FunTy (TyConApp GHC.Base.Functor [TyVarTy f]) (AppTy (TyVarTy f) (TyVarTy a)) Term: TyConApp [] [TyConApp GHC.Types.Bool []] Vars: [f,a] Nothing *CheckType> matchHole "map" 1 "[True]" Hole: TyConApp [] [TyVarTy a] Term: TyConApp [] [TyConApp GHC.Types.Bool []] Vars: [a] Just (TvSubst InScopeSet [(adpV,a)] [(adpV,TyConApp GHC.Types.Bool [])]) *CheckType>