Opened 4 months ago

Closed 4 months ago

Last modified 3 months ago

#8630 closed bug (wontfix)

Kind inference fails to account for associated types

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.7
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:

Description

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.

Change History (3)

comment:1 Changed 4 months ago by simonpj

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.

comment:2 Changed 4 months ago by goldfire

  • Resolution set to wontfix
  • Status changed from new to 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.

comment:3 Changed 3 months ago by Richard Eisenberg <eir@…>

In 0369c9745e2ce66f4c2d817a3aa9f2487395e0c7/ghc:

Clarify issue in #8630 in users' guide.

We do *not* propagate kind information from an instance declaration's
members back into the instance head.
Note: See TracTickets for help on using tickets.