Data family instance with visible forall in return kind is incorrectly rejected
GHC 8.10 and later reject this program:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Kind
data family Hm :: forall a -> a -> Type
data instance Hm :: forall a -> a -> Type
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:1: error:
• Expecting one more argument to ‘Hm’
Expected kind ‘a -> *’, but ‘Hm’ has kind ‘forall a -> a -> *’
• In the data instance declaration for ‘Hm’
|
11 | data instance Hm :: forall a -> a -> Type
| ^^^^^^^^^^^^^^^^
I claim that this should be accepted, however. This is especially strange since GHC does accept this program if Hm
is changed from a data family to a normal data type:
data Hm :: forall a -> a -> Type
The culprit is this code in tcDataFamInstHeader
:
-- See Note [Result kind signature for a data family instance]
tc_kind_sig (Just hs_kind)
= do { sig_kind <- tcLHsKindSig data_ctxt hs_kind
; let (tvs, inner_kind) = tcSplitForAllTys sig_kind
; lvl <- getTcLevel
; (subst, _tvs') <- tcInstSkolTyVarsAt lvl False emptyTCvSubst tvs
-- Perhaps surprisingly, we don't need the skolemised tvs themselves
; return (substTy subst inner_kind) }
The use of tcSplitForAllTys
above incorrectly splits off the forall a
in forall a -> a -> Type
, but really, we should only be splitting off invisible forall
s in the result kind. Changing tcSplitForAllTys
to tcSplitForAllTysInvis
would fix this issue.
In fact, there are a number of places where we ought to use tcSplitForAllTysInvis
instead of tcSplitForAllTys
. This was originally noticed in !4417 (comment 311329), but this bug can be understood independently of !4417 (closed).