A cast might get in the way of instantiation
Suppose we have a type signature f :: forall a. Eq a => blah
, and it somehow kindchecks to
forall a. ((Eq a => Blah) > co)
In principle this can happen:
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
= do { ctxt' < tc_hs_context mode ctxt
; ek < newOpenTypeKind  The body kind (result of the function) can
 be TYPE r, for any r, hence newOpenTypeKind
; ty' < tc_lhs_type mode rn_ty ek
; checkExpectedKind (unLoc rn_ty) (mkPhiTy ctxt' ty')
liftedTypeKind exp_kind }
That checkExpectedKind
can add a cast.
If this happens, our instantiation mechanisms would fall over in a heap. We'd instantiate the forall a
, but then fail to instantiate the Eq a =>
; instead we'd unify (Eq a => blah) > co
with the function body. Bad, bad.
This popped up when fixing #18008 (closed), when a missing zonk in tcHsPartialSigType
was producing just such a forall (with a Refl coercion). But it seems plausible that it could happen for real.
EDIT: And it does:
{# LANGUAGE KindSignatures, TypeFamilies, DataKinds #}
module Bug where
import Data.Kind ( Type )
type family Star where
Star = Type
f :: ((Eq a => a > Bool) :: Star)
f x = x == x
produces
Bug.hs:11:1: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
a0 :: *
Eq a :: Constraint
Expected type: Eq a => a > Bool
Actual type: a0 > Bool
• The equation(s) for ‘f’ have one argument,
but its type ‘Eq a => a > Bool’ has none
• Relevant bindings include
f :: Eq a => a > Bool (bound at Bug.hs:11:1)

11  f x = x == x
 ^^^^^^^^^^^^
Solution: teach instantiation to look through casts.