Don't infer forall with an escaping kind
This ticket is really a subtask of #20686; I am creating a separate ticket since it's not about defaulting and in theory could be done separately.
Given this program
module M1 where
import GHC.Exts
f = f :: (_ :: TYPE (r s))
GHC fails:
M1.hs:5:1: error: [GHC-31147]
• Quantified type's kind mentions quantified type variable
type: ‘forall {k} {r :: k -> RuntimeRep} {s :: k}
{t :: TYPE (r s)}.
t’
where the body of the forall has this kind: ‘TYPE (r s)’
However, this failure happens too late: we have inferred a type for f
that shouldn't exist in the first place. Quoting #23051 (comment 484810):
GHC is forming bad types, like
forall f g (a :: TYPE (f g)). a
, whose kind mentions free type variables. These types are errored upon inValidity.checkEscapingKind
, but they shouldn't ever exist in the first place, as they violate the PKTI ofNote [The Purely Kinded Type Invariant (PKTI)]
. We mused on the call about using levels to ensure this property. I think this could work, but it's a bit indirect. Perhaps better (and simpler) would be just to instruct e.g.candidateQTyVarsOfTypes
not to consider variables free in a type's kind as candidates for generalization. (The "e.g." is because there are several entry points to this algorithm; they'd all likely need to be updated. Note: entry points, not the recursive worker. This property is not recursive!) The candidate-gathering algorithm already tracks a set of bound variables not to consider as candidates, but these variables also are used to detect so-called "naughty" quantification, which is not what we're concerned about here. So we'd need a new set of variables-to-avoid. Once these variables are not quantified over, they will get promoted, and I think all will work smoothly. This is like Simon's idea (on the call) of adding the kind variables to the mono-tyvars, but covers bothsimplifyInfer
andkindGeneralize
, instead of just the former.
I think a better plan would be to promote any free meta-tyvars of the kind, before calling
candidateQTyVarOfTypes
. It already knows not to quantify over tyvars from an outer level.
As a result of this ticket, we should not form the bad type and remove the call checkEscapingKind
in GHC.Tc.Gen.Bind
; the error for the above program will be different.
Here are two other testcases that construct a forall with an escaping kind:
module M2 where
import GHC.Exts
f :: (_ :: TYPE r)
f = f
{-# LANGUAGE TemplateHaskell, PartialTypeSignatures #-}
module M3 where
import M3aux
h = $$g
{-# LANGUAGE TemplateHaskell, PartialTypeSignatures #-}
module M3aux where
import Data.Kind
import GHC.Exts
import Language.Haskell.TH (Code, Q)
g :: Code Q _
g = [||let f :: forall (r :: Type -> RuntimeRep) s (a :: TYPE (r s)). () -> a
f = f
in f () ||]
Relevant notes: Note [Inferred type with escaping kind]
, Note [Check for escaping result kind]
.