Kind inference fails to account for associated types

Consider this:

{-# LANGUAGE PolyKinds, TypeFamilies, FlexibleInstances #-}

class C a where
  type F a

instance C a where
  type F a = a -> a

HEAD gives me

    Expected a type, but ‛a’ has kind ‛k’
    In the type ‛a -> a’
    In the type instance declaration for ‛F’
    In the instance declaration for ‛C a’

The problem is that the use of (->) in the RHS of the definition for the F a instance constrains a to be of kind *, but GHC does not propagate this information back to the instance head. This decision is in conflict with the behavior for class declarations (as opposed to instance declarations), where a type variable's use in the definition informs its kind in the head.

Trac metadata

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

changed weight to 5

added Tbug Trac import typechecker labels

I suppose you are right here. But I think it'll take quite a bit of code to do the Right Thing here. The Right Thing is, I suppose, to walk over the associated-type declarations of the instance, and gather any kind constraints they generate. But consider something like this:

instance C (T a) where
  type F (T a) b = b -> a

Here we must bring 'b' into scope before doing kind-checking on the RHS of the type instance. And then there are data families. This all duplicates the code we subsequently use for typechecking those type/data instances. Fiddly.

Moreover, you could argue the same for value declarations too:

instance C (T a) where
   op x y = [x, y::a -> a]

There's a type signature deep in the term that constrains the kind of 'a'. It would arguably be inconsistent to look at type instances but not value instances. And we really really are not going to look into the value terms!

So I'm not sure it's worth fixing this.

closed

Fair enough. I took a look at what it would take to fix this, too, and came to much the same conclusion. I was rather hoping you might see some refactoring that would fix this bug and simplify gobs of other code in the process, as you sometimes do. When I have a chance, I might see if this behavior can be documented somewhere, as it did truly confuse me when I first hit it.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedWon'tFix

mentioned in commit 0369c974

added Pnormal label