Does the sub-type check in Note [Impedance matching] ever fail?
GHC.Tc.Gen.Bind
tells us
Note [Impedance matching]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f 0 x = x
f n x = g [] (not x)
g [] y = f 10 y
g _ y = f 9 y
After typechecking we'll get
f_mono_ty :: a -> Bool -> Bool
g_mono_ty :: [b] -> Bool -> Bool
with constraints
(Eq a, Num a)
Note that f is polymorphic in 'a' and g in 'b'; and these are not linked.
The types we really want for f and g are
f :: forall a. (Eq a, Num a) => a -> Bool -> Bool
g :: forall b. [b] -> Bool -> Bool
We can get these by "impedance matching":
tuple :: forall a b. (Eq a, Num a) => (a -> Bool -> Bool, [b] -> Bool -> Bool)
tuple a b d1 d1 = let ...bind f_mono, g_mono in (f_mono, g_mono)
f a d1 d2 = case tuple a Any d1 d2 of (f, g) -> f
g b = case tuple Integer b dEqInteger dNumInteger of (f,g) -> g
Suppose the shared quantified tyvars are qtvs and constraints theta.
Then we want to check that
forall qtvs. theta => f_mono_ty is more polymorphic than f's polytype
and the proof is the impedance matcher.
Notice that the impedance matcher may do defaulting. See #7173.
It also cleverly does an ambiguity check; for example, rejecting
f :: F a -> F a
where F is a non-injective type function.
This describes a sub-type check. That sub-type check is performed with the context returned from this function:
mk_impedance_match_msg :: MonoBindInfo
-> TcType -> TcType
-> TidyEnv -> TcM (TidyEnv, SDoc)
-- This is a rare but rather awkward error messages
mk_impedance_match_msg (MBI { mbi_poly_name = name, mbi_sig = mb_sig })
inf_ty sig_ty tidy_env
= do { (tidy_env1, inf_ty) <- zonkTidyTcType tidy_env inf_ty
; (tidy_env2, sig_ty) <- zonkTidyTcType tidy_env1 sig_ty
; let msg = vcat [ text "When checking that the inferred type"
, nest 2 $ ppr name <+> dcolon <+> ppr inf_ty
, text "is as general as its" <+> what <+> text "signature"
, nest 2 $ ppr name <+> dcolon <+> ppr sig_ty ]
; return (tidy_env2, msg) }
where
what = case mb_sig of
Nothing -> text "inferred"
Just sig | isPartialSig sig -> text "(partial)"
| otherwise -> empty
A search in the testsuite shows no occurrence of "When checking that the inferred type".
So: Does this sub-type check ever fail? If so, we should have a test case in the testsuite for this message. If not, we should explain why failure is impossible and then remove the above function.