Empty constraint tuples are mis-kinded

See #11621

Consider

-- If :: forall k. 'Bool -> k -> k -> k
type family If cond tru fls where
   If True tru fls = tru
   If False tru fls = fls

foo :: If True () (Eq a) => a -> a
foo = error "urk"

This should work fine. But we get

Foo.hs:8:21:
    The third argument of `If' should have kind `*',
      but `Eq a' has kind `Constraint'
    In the type signature for `foo': foo :: If True () (Eq a) => a -> a

Reason: GHC is treating the () unit tuple as of kind *.

Reason is that in the HsTupleTy case of tc_hs_type in TcHsType, we see

         -- In the [] case, it's not clear what the kind is, so guess *

And that guess is plain wrong in this case. Unfortunately I don't see an easy fix, but it's plain wrong as-is.

Simon

---

Edit by @sgraf812: Full reproducer with SAKS

{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, MultiParamTypeClasses, TypeFamilies, StandaloneKindSignatures, RankNTypes, PolyKinds #-}

module T9547 where

import GHC.Exts

type If :: forall k. Bool -> k -> k -> k
type family If cond tru fls where
   If True tru fls = tru
   If False tru fls = fls

foo :: If True () (Eq a) => a -> a
foo = error "urk"

Trac metadata

Trac field	Value
Version	7.8.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture