Opened 10 years ago

Closed 10 years ago

#2855 closed feature request (duplicate)

Surprising type (family) type derived

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: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Consider the following module

{-# LANGUAGE TypeFamilies #-}
module Bug5 where

class C a where
    type T a
    f :: T a -> T a -> T a

data D a = D { t :: T a }

g r = f (t r) (t r)

Now ask for the type of g

*Bug5> :t g
g :: (T a ~ T a1, C a1) => D a -> T a1

Why isn't the type

g :: (C a) => D a -> T a

?

The strange type is a minor nuisance, but it gets worse

{-# LANGUAGE TypeFamilies #-}
module Bug6 where

class C a where
    type T a
    type U a
    f :: T a -> T a -> T a
    x :: U a -> T a

data D a = D { t :: T a, u :: U a }

g r = f (t r) (x (u r))

This doesn't type check at all.

An even simpler example that fails:

{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
module Bug7 where

class C a where
    type T a
    type U a
    x :: U a -> T a

data D a = D (U a)

g :: (C a) => D a -> T a
g (D u) = x u

Change History (6)

comment:1 Changed 10 years ago by guest

Here's more of the same kind:

{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
module Bug8 where

class C a where
    type T a
    type U a
    x :: U a -> T a

--foo :: (C a) => U a -> T a
foo ua = x ua

This compiles, and the type of foo is the one in the signature. But if the signature is included there are type errors.

comment:2 Changed 10 years ago by simonpj

difficulty: Unknown
Type: bugfeature request

I'm afraid these aren't bugs. They all arise because type synonym families (unlike data type families) do not have to be injective. For example you ask re Bug5 why GHC doesn't get the type

g :: (C a) => D a -> T a

Answer: because that's not the most general type. The type GHC gives is strictly more general. Suppose

type instance T Int = Char
type instance T Bool = Char

then T Int ~ T Bool, but of course Int and Bool are different types.

The other examples you give are more tiresome. For example:

class C a where
    type T a
    type U a
    x :: U a -> T a

data D a = D (U a)

g :: (C a) => D a -> T a
g (D u) = x u

We know that (u :: U a), but at what type should we call the polymorphic function x? Let's say at some type a1. Then since x is applied to u we know that U a should be the same type as U a1, but that does not require a to be the same type as a1, as we saw above.

In this case, it's vexing because the only solution to (U a ~ U a1), where (i) a is a skolem constant, and (ii) no other equality constraints are available to solve it, is a~a1. But GHC doesn't do that kind of "the only solution" reasoning. Yet anyway.

In general, a function with a polymorphic type variable that occurs only under a type function is likely to give rise to this kind of trouble.

We're also thinking about allowing you to declare theat a type function is injective, which would solve this problem in a different way.

I hope that explains it a bit. I'll leave this open as a feature request... perhaps for injective type functions. (Although I'm not sure whether that'd work in your application.)

Simon

comment:3 Changed 10 years ago by guest

So what about my attached last example? It's another one of these the type that ghc reports cannot be inserted in the code. Very frustrating.

You say "At what type should we call the poymorphic function x?" Well, I want it to be the x from the dictionary (C a) that I'm passing. So there is no doubt at what type it should be called, it's at type (U a). I guess there's no way to express that.

This is very annoying, because it means that the associated types simply don't work for some of the tasks that I thought they were supposed to solve. I can provide a real life example if that helps.

comment:4 Changed 10 years ago by simonpj

Several things going on here. Concerning type signatures, it's indeed annoying that a program can have an inferred type that can't be used as a type signature. I plan to fix that by rejecting both programs. You won't like that, but it's silly to accept one but not the other. I think there's a ticket open for this, but I'm not sure which one...

Concering "I want it to be the x from the dictionary (C a) that I'm passing". Yes, I know. That's why I said it's vexing; indeed, the solution you suggest is the only solution that will work. All I'm saying is that this is a new form of reasoning, which GHC does not in any way implement at the moment. It'd take a bit of study to figure out how to do it, or indeed if there is any well-behaved, principal solution. If you can work one out, do tell us!

Can you not design your functions so that they take at least one parameter that does not live inside a type-function application? Or, would you be willing for your type functions to be injective, or would that be too restrictive for your application?

Simon

comment:5 Changed 10 years ago by chak

This is a duplicate of #1897, is it not?

As far as I am concerned, I still think, we should solve this problem in the way Lennart proposed when we discussed this last: http://www.mail-archive.com/haskell-cafe@haskell.org/msg39774.html (after type inference, do type checking again with the inferred signatures).

comment:6 Changed 10 years ago by simonpj

Resolution: duplicate
Status: newclosed

Yes, it's a dup. So I'll close it now, having linked from #1897

Simon

Note: See TracTickets for help on using tickets.