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.