GHC Handbook

Note [Failure in local type signatures]

GHC/Tc/Solver.hs:291 compiler 6 tickets 

When kind checking a type signature, we like to fail fast if we can't
solve all the kind equality constraints, for two reasons:

  * A kind-bogus type signature may cause a cascade of knock-on
    errors if we let it pass

  * More seriously, we don't have a convenient term-level place to add
    deferred bindings for unsolved kind-equality constraints.  In
    earlier GHCs this led to un-filled-in coercion holes, which caused
    GHC to crash with "fvProv falls into a hole" See #11563, #11520,
    #11516, #11399

But what about /local/ type signatures, mentioning in-scope type
variables for which there might be 'given' equalities?  For these we
might not be able to solve all the equalities locally. Here's an
example (T15076b):

  class (a ~ b) => C a b
  data SameKind :: k -> k -> Type where { SK :: SameKind a b }

  bar :: forall (a :: Type) (b :: Type).
         C a b => Proxy a -> Proxy b -> ()
  bar _ _ = const () (undefined :: forall (x :: a) (y :: b). SameKind x y)

Consider the type signature on 'undefined'. It's ill-kinded unless
a~b.  But the superclass of (C a b) means that indeed (a~b). So all
should be well. BUT it's hard to see that when kind-checking the signature
for undefined.  We want to emit a residual (a~b) constraint, to solve
later.

Another possibility is that we might have something like
   F alpha ~ [Int]
where alpha is bound further out, which might become soluble
"later" when we learn more about alpha.  So we want to emit
those residual constraints.

BUT it's no good simply wrapping all unsolved constraints from
a type signature in an implication constraint to solve later. The
problem is that we are going to /use/ that signature, including
instantiate it.  Say we have
     f :: forall a.  (forall b. blah) -> blah2
     f x = <body>
To typecheck the definition of f, we have to instantiate those
foralls.  Moreover, any unsolved kind equalities will be coercion
holes in the type.  If we naively wrap them in an implication like
     forall a. (co1:k1~k2,  forall b.  co2:k3~k4)
hoping to solve it later, we might end up filling in the holes
co1 and co2 with coercions involving 'a' and 'b' -- but by now
we've instantiated the type.  Chaos!

Moreover, the unsolved constraints might be skolem-escape things, and
if we proceed with f bound to a nonsensical type, we get a cascade of
follow-up errors. For example polykinds/T12593, T15577, and many others.

So here's the plan (see tcHsSigType):

* pushLevelAndSolveEqualitiesX: try to solve the constraints

* kindGeneraliseSome: do kind generalisation

* buildTvImplication: build an implication for the residual, unsolved
  constraint

* simplifyAndEmitFlatConstraints: try to float out every unsolved equality
  inside that implication, in the hope that it constrains only global
  type variables, not the locally-quantified ones.

  * If we fail, or find an insoluble constraint, emit the implication,
    so that the errors will be reported, and fail.

  * If we succeed in floating all the equalities, promote them and
    re-emit them as flat constraint, not wrapped at all (since they
    don't mention any of the quantified variables.

* Note that this float-and-promote step means that anonymous
  wildcards get floated to top level, as we want; see
  Note [Checking partial type signatures] in GHC.Tc.Gen.HsType.

All this is done:

* In GHC.Tc.Gen.HsType.tcHsSigType, as above

* solveEqualities. Use this when there no kind-generalisation
  step to complicate matters; then we don't need to push levels,
  and can solve the equalities immediately without needing to
  wrap it in an implication constraint.  (You'll generally see
  a kindGeneraliseNone nearby.)

* In GHC.Tc.TyCl and GHC.Tc.TyCl.Instance; see calls to
  pushLevelAndSolveEqualitiesX, followed by quantification, and
  then reportUnsolvedEqualities.

  NB: we call reportUnsolvedEqualities before zonkTcTypeToType
  because the latter does not expect to see any un-filled-in
  coercions, which will happen if we have unsolved equalities.
  By calling reportUnsolvedEqualities first, which fails after
  reporting errors, we avoid that happening.

See also #18062, #11506

References 1

Referenced by 10