Opened 5 years ago

Closed 5 years ago

Last modified 5 years ago

#2852 closed bug (worksforme)

Type family checking oddity

Reported by: guest Owned by:
Priority: normal Milestone:
Component: Compiler Version: 6.10.1
Keywords: Cc: lennart@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Difficulty:
Test Case: Blocked By:
Blocking: Related Tickets:

Description

Consider the following snipped

class C a where
    type T a

data D a = D (T a)

If we now ask for the type of D we get

> :t D
D :: T a -> D a

I find this odd. The type T is in class C, so why is there no context on D saying so? It would be natural.

Now try some expression

> D True
<interactive>:1:2:
    Couldn't match expected type `T a' against inferred type `Bool'
    In the first argument of `D', namely `True'
    In the expression: D True
    In the definition of `it': it = D True

But this isn't really type incorrect, we just don't know yet. To remedy the problem we can use a context on the data declaration.

data (C a) => D a = D (T a)

And we try again

> :t D True
D True :: (Bool ~ T a, C a) => D a

This is what I would have expected in the first try as well; a context indicating what must hold for this to be type correct.

Change History (4)

comment:1 Changed 5 years ago by guest

  • Cc lennart@… added

comment:2 in reply to: ↑ description Changed 5 years ago by chak

  • Resolution set to worksforme
  • Status changed from new to closed

Replying to guest:

Consider the following snipped

class C a where
    type T a

data D a = D (T a)

If we now ask for the type of D we get

> :t D
D :: T a -> D a

I find this odd. The type T is in class C, so why is there no context on D saying so? It would be natural.

In the first proposal of associated types, we used to require such a context, but subsequently decided that there is really no basis for this requirement. Take this definition:

myid :: T a -> T a
myid x = x

Why should we require a C a context here? No class methods are used, no evidence is needed.

Also, what if your definition would have been

newtype D a = D (T a)

Then, D cannot have a context.

In the case of associated data declarations it would actually be rather inconvenient to require contexts. Say, we have

class D a where
  data DT a

We might want to use DT partially applied, as in F D, where F :: (* -> *) -> *. What context should we use here?

So, the right way to think of an associated type

class C a where
  type T a

is as syntactic sugar for

type family T a
class C a

It's convenient to bundle families that are defined in lock step with a class as an associated types. You get a warning if you forget to define the family instance in a class instance and it highlights the structure of your code for a human reader. (And it allows for associated synonym defaults.) However, there is really nothing semantically deep about associating a family with a class.

Now try some expression

> D True
<interactive>:1:2:
    Couldn't match expected type `T a' against inferred type `Bool'
    In the first argument of `D', namely `True'
    In the expression: D True
    In the definition of `it': it = D True

But this isn't really type incorrect, we just don't know yet. To remedy the problem we can use a context on the data declaration.

data (C a) => D a = D (T a)

And we try again

> :t D True
D True :: (Bool ~ T a, C a) => D a

This is what I would have expected in the first try as well; a context indicating what must hold for this to be type correct.

You forgot the :t in front of the D True the first time around. Works fine with me in 6.10.1 and the HEAD:

*Main> :t D True
D True :: (Bool ~ T a) => D a

So, I think, this was only a typo during the ghci interaction. Hence, closing the ticket.

comment:3 Changed 5 years ago by guest

Fair enough. As the summary said, this was more an oddity than a bug.
I'd say it's still somewhat surprising to use something (the type) from a class and not get the context, but I see the technical reasons for leaving it out.

comment:4 Changed 5 years ago by guest

Note: See TracTickets for help on using tickets.