A cast might get in the way of instantiation

Suppose we have a type signature f :: forall a. Eq a => blah, and it somehow kind-checks 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.