Inconsistency between SAKs and inference

Consider

{-# LANGUAGE CUSKs, TypeFamilies, EmptyDataDecls, PolyKinds, KindSignatures, StandaloneKindSignatures #-}

module Foo where

import Data.Kind

class C f where
   type S (f :: turtle)
   type T f

This is accepted today. But try adding a stand-alone kind signature (with the correct kind!):

type C :: wombat -> Constraint

and the same program is rejected with

Foo.hs:10:4: error:
    • Expected kind ‘wombat’, but ‘f’ has kind ‘turtle’
      ‘turtle’ is a rigid type variable bound by
        the associated type family declaration for ‘S’
        at Foo.hs:10:12-22
      ‘wombat’ is a rigid type variable bound by
        the associated type family declaration for ‘S’
        at Foo.hs:7:11-30
    • In the associated type family declaration for ‘S’
   |
10 |    type S (f :: turtle)
   |    ^^^^^^^^^^^^^^^^^^^^

This seems inconsistent.

Diagnosis

The reason this happens with a standalone kind signature is because kcCheckDeclHeader_sig looks at

• the kind signature C :: wombat -> Constraint,
• the class header for C, namely class C f where, and gives C the final skolem tyvars [wombat, f::wombat].

Then check_initial_kind_assoc uses the CUSK strategy to kind-check S; and that in turn uses a skolem for turtle, which doesn't unify with wombat.

On the other hand, without the standalone kind signature we accept it because we kind-check the class and associated types together, rather than doing the class first and then the associated types.

Discussion

Consider a CUSK version of the same program:

class C (f :: turtle) where
   type S (f :: wombat) :: Type

This is rejected today, with the same message as above, on the grounds that wombat is a local alias for turtle. This treatment is inconsistent with the term level where we allow

f1 :: forall a. a -> blah
f1 (x :: b) = ...   -- b is a local alias for a

On the other hand, we also reject

data T (a :: p) (b :: q) = MkT (SameKind a b)

where SameKind :: k -> k -> Type. You could argue that p and q are both aliases for the same kind variable (k? p?); and that would be consistent with the term level where we allow

f2 :: forall a. a -> a -> blah
f2 (x :: b) (y :: c) = ...   -- b and c are both local aliases for a.

But I hate the definition of T because it looks so outright misleading. (I hate f2 as well, just not so much.) The principle is, I think, that variables brought into scope simultaneously should not be aliases for each other. Nested scopes are a different matter.

Conclusion

I'm content with the treatment for

• inference (right at the top_)
• CUSKs (rejecting aliases) but not with that for standalone kind signatures (as above). Given

type C :: wombat -> Constraint
class C f where
   type S (f :: turtle)
   type T f

I think we should accept this, with turtle as the name of the scoped variable.