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.