Manuel said earlier that the source of the problem here is foo's ambiguous type signature (I'm switching back to the original, simplified example). Type checking with ambiguous type signatures is hard because the type checker has to guess types and this guessing step may lead to too many (ambiguous) choices. But this doesn't mean that this worst case scenario always happens. Consider your example again type family Id a type instance Id Int = Int foo :: Id a -> Id a foo = id foo' :: Id a -> Id a foo' = foo The type checking problem for foo' boils down to verifying the formula forall a. exists b. Id a ~ Id b Of course for any a we can pick b=a to make the type equation statement hold. Fairly easy here but the point is that the GHC type checker doesn't do any guessing at all. The only option you have (at the moment, there's still lots of room for improving GHC's type checking process) is to provide some hints, for example mimicking System F style type application by introducing a type proxy argument in combination with lexically scoped type variables. foo :: a -> Id a -> Id a foo _ = id foo' :: Id a -> Id a foo' = foo (undefined :: a) Martin Ganesh Sittampalam wrote:

On Wed, 9 Apr 2008, Manuel M T Chakravarty wrote:

...

Sittampalam, Ganesh:

...

...

No, I meant can't it derive that equality when matching (Id a) against (Id b)? As you say, it can't derive (a ~ b) at that point, but (Id a ~ Id b) is known, surely?

No, it is not know. Why do you think it is?

Well, if the types of foo and foo' were forall a . a -> a and forall b . b -> b, I would expect the type-checker to unify a and b in the argument position and then discover that this equality made the result position unify too. So why can't the same happen but with Id a and Id b instead?

...

The problem is really with foo and its signature, not with any use of foo. The function foo is (due to its type) unusable. Can't you change foo?

Here's a cut-down version of my real code. The type family Apply is very important because it allows me to write class instances for things that might be its first parameter, like Id and Comp SqlExpr Maybe, without paying the syntactic overhead of forcing client code to use Id/unId and Comp/unComp. It also squishes nested Maybes which is important to my application (since SQL doesn't have them).

castNum is the simplest example of a general problem - the whole point is to allow clients to write code that is overloaded over the first parameter to Apply using primitives like castNum. I'm not really sure how I could get away from the ambiguity problem, given that desire.

Cheers,

Ganesh

{-# LANGUAGE TypeFamilies, GADTs, UndecidableInstances, NoMonomorphismRestriction #-}

newtype Id a = Id { unId :: a } newtype Comp f g x = Comp { unComp :: f (g x) }

type family Apply (f :: * -> *) a

type instance Apply Id a = a type instance Apply (Comp f g) a = Apply f (Apply g a) type instance Apply SqlExpr a = SqlExpr a type instance Apply Maybe Int = Maybe Int type instance Apply Maybe Double = Maybe Double type instance Apply Maybe (Maybe a) = Apply Maybe a

class DoubleToInt s where castNum :: Apply s Double -> Apply s Int

instance DoubleToInt Id where castNum = round

instance DoubleToInt SqlExpr where castNum = SECastNum

data SqlExpr a where SECastNum :: SqlExpr Double -> SqlExpr Int

castNum' :: (DoubleToInt s) => Apply s Double -> Apply s Int castNum' = castNum

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

I think it's not fair to say TFs as implemented in GHC are broken. Fine, they are situations where the current implementation is overly conservative. The point is that the GHC type checker relies on automatic inference. Hence, there'll always be cases where certain "reasonable" type signatures are rejected. For example, consider the case of "undecidable" and "non-confluent" type class instances. instance Foo a => Bar a -- (1) instance Erk a => Bar [a] -- (2) GHC won't accept the above type class instance (note: instances are a kind of type signature) because - instance (1) is potentially non-terminating (the size of the type term is not decreasing) - instance (2) overlaps with (1), hence, it can happen that during context reduction we choose the "wrong" instance. To conclude, any system with automatic inference will necessary reject certain type signatures/instances in order to guarantee soundness, completeness and termination. Lennart, you said

(It's also pretty easy to fix the problem.)

What do you mean? Easy to fix the type checker, or easy to fix the program by inserting annotations to guide the type checker? Martin Lennart Augustsson wrote:

Let's look at this example from a higher level.

Haskell is a language which allows you to write type signatures for functions, and even encourages you to do it. Sometimes you even have to do it. Any language feature that stops me from writing a type signature is in my opinion broken. TFs as implemented in currently implemented ghc stops me from writing type signatures. They are thus, in my opinion, broken.

A definition should either be illegal or it should be able to have a signature. I think this is a design goal. It wasn't true in Haskell 98, and it's generally agreed that this was a mistake.

To summarize: I don't care if the definition is useless, I want to be able to give it a type signature anyway.

(It's also pretty easy to fix the problem.)

-- Lennart

On Wed, Apr 9, 2008 at 7:20 AM, Martin Sulzmann mailto:martin.sulzmann@gmail.com> wrote:

Manuel said earlier that the source of the problem here is foo's ambiguous type signature (I'm switching back to the original, simplified example). Type checking with ambiguous type signatures is hard because the type checker has to guess types and this guessing step may lead to too many (ambiguous) choices. But this doesn't mean that this worst case scenario always happens.

Consider your example again

type family Id a

type instance Id Int = Int

foo :: Id a -> Id a foo = id

foo' :: Id a -> Id a foo' = foo

The type checking problem for foo' boils down to verifying the formula

forall a. exists b. Id a ~ Id b

Of course for any a we can pick b=a to make the type equation statement hold. Fairly easy here but the point is that the GHC type checker doesn't do any guessing at all. The only option you have (at the moment, there's still lots of room for improving GHC's type checking process) is to provide some hints, for example mimicking System F style type application by introducing a type proxy argument in combination with lexically scoped type variables.

foo :: a -> Id a -> Id a foo _ = id

foo' :: Id a -> Id a foo' = foo (undefined :: a)

Martin

Ganesh Sittampalam wrote:

On Wed, 9 Apr 2008, Manuel M T Chakravarty wrote:

Sittampalam, Ganesh:

No, I meant can't it derive that equality when matching (Id a) against (Id b)? As you say, it can't derive (a ~ b) at that point, but (Id a ~ Id b) is known, surely?

No, it is not know. Why do you think it is?

Well, if the types of foo and foo' were forall a . a -> a and forall b . b -> b, I would expect the type-checker to unify a and b in the argument position and then discover that this equality made the result position unify too. So why can't the same happen but with Id a and Id b instead?

The problem is really with foo and its signature, not with any use of foo. The function foo is (due to its type) unusable. Can't you change foo?

Here's a cut-down version of my real code. The type family Apply is very important because it allows me to write class instances for things that might be its first parameter, like Id and Comp SqlExpr Maybe, without paying the syntactic overhead of forcing client code to use Id/unId and Comp/unComp. It also squishes nested Maybes which is important to my application (since SQL doesn't have them).

castNum is the simplest example of a general problem - the whole point is to allow clients to write code that is overloaded over the first parameter to Apply using primitives like castNum. I'm not really sure how I could get away from the ambiguity problem, given that desire.

Cheers,

Ganesh

{-# LANGUAGE TypeFamilies, GADTs, UndecidableInstances, NoMonomorphismRestriction #-}

newtype Id a = Id { unId :: a } newtype Comp f g x = Comp { unComp :: f (g x) }

type family Apply (f :: * -> *) a

type instance Apply Id a = a type instance Apply (Comp f g) a = Apply f (Apply g a) type instance Apply SqlExpr a = SqlExpr a type instance Apply Maybe Int = Maybe Int type instance Apply Maybe Double = Maybe Double type instance Apply Maybe (Maybe a) = Apply Maybe a

class DoubleToInt s where castNum :: Apply s Double -> Apply s Int

instance DoubleToInt Id where castNum = round

instance DoubleToInt SqlExpr where castNum = SECastNum

data SqlExpr a where SECastNum :: SqlExpr Double -> SqlExpr Int

castNum' :: (DoubleToInt s) => Apply s Double -> Apply s Int castNum' = castNum

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org mailto:Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org mailto:Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Claus Reinke wrote:

...

The point is that the GHC type checker relies on automatic inference. Hence, there'll always be cases where certain "reasonable" type signatures are rejected. .. To conclude, any system with automatic inference will necessary reject certain type signatures/instances in order to guarantee soundness, completeness and termination.

i think Lennart's complaint is mainly about cases where GHC does not accept the very type signature it infers itself. all of which cases i'd consider bugs myself, independent of what type system feature they are related to.

there are also the related cases of type signatures which cannot be expressed in the language but which might occur behind the scenes. all of these cases i'd consider language limitations that ought to be removed.

the latter cases also mean that type errors are reported either in a syntax that can not be used in programs or in a misleading external syntax that does not fully represent the internal type.

in this example, ghci infers a type for foo' that it rejects as a type signature for foo'. so, either the inferred type is inaccurately presented, or there's a gap in the type system, between inferred and declared types, right?

Good point(s) which I missed earlier. Type inference (no annotations) is easy but type checking is much harder. Type checking is not all about pure checking, we also perform some inference, the Hindley/Milner unification variables which arise out of the program text (we need to satisfy these constraints via the annotation). To make type checking easier we should impose restrictions on inference. We (Tom/SimonPJ/Manuel) thought about this possibility. The problem is that it's hard to give an intuitive, declarative description of those restrictions. Martin

Lennart Augustsson:

On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann

...

wrote:

Lennart, you said

(It's also pretty easy to fix the problem.)

What do you mean? Easy to fix the type checker, or easy to fix the program by inserting annotations to guide the type checker?

Martin

I'm referring to the situation where the type inferred by the type checker is illegal for me to put into the program. In our example we can fix this in two ways, by making foo' illegal even when it has no signature, or making foo' legal even when it has a signature.

To make it illegal: If foo' has no type signature, infer a type for foo', insert this type as a signature and type check again. If this fails, foo' is illegal.

That would be possible, but it means we have to do this for all bindings in a program (also all lets bindings etc).

To make it legal: If foo' with a type signature doesn't type check, try to infer a type without a signature. If this succeeds then check that the type that was inferred is alpha-convertible to the original signature. If it is, accept foo'; the signature doesn't add any information.

This harder, if not impossible. What does it mean for two signatures to be "alpha-convertible"? I assume, you intend that given type S a = Int the five signatures forall a. S a forall b. S b forall a b. S (a, b) Int S Int are all the "alpha-convertible". Now, given type family F a b type instance F Int c = Int what about forall a. F a Int forall a. F Int Int forall a. F Int a forall a b. (a ~ Int) => F a b <and so on> So, I guess, you don't really mean alpha-convertible in its original syntactic sense. We should accept the definition if the inferred and the given signature are in some sense "equivalent". For this "equivalence" to be robust, I am sure we need to define it as follows, where <= is standard type subsumption: t1 "equivalent" t2 iff t1 <= t2 and t2 <= t1 However, the fact that we cannot decide type subsumption for ambiguous types is exactly what led us to the original problem. So, nothing has been won. Summary ~~~~~~~ Trying to make those definitions that are currently only legal *without* a signature also legal when the inferred signature is added (foo' in Ganesh's example) doesn't seem workable. However, to generally reject the same definitions, even if they are presented without a signature, seems workable. It does require the compiler to compute type annotations, and then, check that it can still accept the annotated program. This makes the process of type checking together with annotating the checked program idempotent, which is nice. Manuel

Lennart Augustsson:

...

wrote:

On Thu, Apr 10, 2008 at 4:20 AM, Manuel M T Chakravarty

forall a. S a forall b. S b forall a b. S (a, b) Int S Int

By alpha-convertible I mean the usual thing from lambda calculus, they are identical modulo the names of bound variables. So only the first two are alpha-convertible to each other.

If you involve any kind of reduction the equivalence test is no longer trivial.

All I'm asking for really, is to be able to paste in the type that was inferred as the signature, without the compiler complaining.

I think a trivial, purely syntactic test, such as the one proposed, would generate at least as much puzzlement as the current situation does. It would mean, you could not have String in your signature if the inferred signature has [Char]. I don't think that this is a solution at all. Manuel

Lennart Augustsson:

On Thu, Apr 10, 2008 at 4:20 AM, Manuel M T Chakravarty

...

wrote: Lennart Augustsson:

On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann

...

wrote:

Lennart, you said

(It's also pretty easy to fix the problem.)

What do you mean? Easy to fix the type checker, or easy to fix the program by inserting annotations to guide the type checker?

Martin

I'm referring to the situation where the type inferred by the type checker is illegal for me to put into the program. In our example we can fix this in two ways, by making foo' illegal even when it has no signature, or making foo' legal even when it has a signature.

To make it illegal: If foo' has no type signature, infer a type for foo', insert this type as a signature and type check again. If this fails, foo' is illegal.

That would be possible, but it means we have to do this for all bindings in a program (also all lets bindings etc).

Of course, but I'd rather the compiler did it than I. It's not that hard, btw. If the whole module type checks, insert all signatures and type check again.

Sure. I did not argue against this. I think it would be a reasonable way forward. Manuel

Lennart Augustsson wrote:

On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann mailto:martin.sulzmann@gmail.com> wrote:

Lennart, you said

(It's also pretty easy to fix the problem.)

What do you mean? Easy to fix the type checker, or easy to fix the program by inserting annotations to guide the type checker?

Martin

I'm referring to the situation where the type inferred by the type checker is illegal for me to put into the program. In our example we can fix this in two ways, by making foo' illegal even when it has no signature, or making foo' legal even when it has a signature.

To make it illegal: If foo' has no type signature, infer a type for foo', insert this type as a signature and type check again. If this fails, foo' is illegal.

To make it legal: If foo' with a type signature doesn't type check, try to infer a type without a signature. If this succeeds then check that the type that was inferred is alpha-convertible to the original signature. If it is, accept foo'; the signature doesn't add any information.

Either of these two option would be much preferable to the current (broken) situation where the inferred signature is illegal.

I understand now what you meant. See my earlier reply to Claus' email. Regarding your request to take into account alpha-convertibility when checking signatures. We know that in GHC the check (forall a, b. Foo a b => a) <= (forall a, c. Foo a c => a) (**) fails cause when testing the constraint/formula derived from the above subsumption check forall a, b. Foo a b implies exists c. Foo a c GHC simply drops the exists c bit and clearly Foo a b does NOT imply Foo a c We need to choose c to be equal to b. I call this process "matching" but it's of course a form of alpha-conversion. (We convince GHC to accept such signatures but encoding System F style type application via redundant type proxy arguments) The point I want to make is that in Chameleon I've implemented a subsumption check which takes into account matching. Therefore, (**) is checkable in Chameleon. BUT matching can be fairly expensive, exponential in the worst case, for example consider cases such as Foo x_i x_i+1 So maybe there's good reason why GHC's subsumption check doesn't take into account matching. The slightly odd thing is that GHC uses a "pessimistic" subsumption check (no matching) in combination with an "optimistic" ambiguity check (see my earlier message on this topic). I'd say it's better to be pessimistic/pessimistic and optimistic/optimistic, maybe this could be a compiler switch? Martin

I didn't say TF was the only broken feature in GHC. But I want to see the broken ones removed, instead of new ones added. :) In the current GHC there are even definitions that are perfecty usable, that cannot be given the type signature that that was inferred. At work we have the warning for missing signatures enabled, and we turn warnings into errors. We have to disbale this for certain definitions, because you cannot give them a signature. I find that broken. -- Lennart On Thu, Apr 10, 2008 at 5:52 AM, Manuel M T Chakravarty < chak@cse.unsw.edu.au> wrote:

Lennart Augustsson:

...

Let's look at this example from a higher level.

Haskell is a language which allows you to write type signatures for functions, and even encourages you to do it. Sometimes you even have to do it. Any language feature that stops me from writing a type signature is in my opinion broken. TFs as implemented in currently implemented ghc stops me from writing type signatures. They are thus, in my opinion, broken.

The problem of ambiguity is not at all restricted to TFs. In fact, you need neither TFs nor FDs to get the exact same behaviour. You don't even need MPTCs:

{-# LANGUAGE FlexibleContexts #-}

...

module Ambiguity where

class C a

bar :: C (a, b) => b -> b bar = id

bar' :: C (a, b) => b -> b bar' = bar

This gives us

/Users/chak/Code/haskell/Ambiguity.hs:10:7:

...

Could not deduce (C (a, b)) from the context (C (a1, b)) arising from a use of `bar' at /Users/chak/Code/haskell/Ambiguity.hs:10:7-9 Possible fix: add (C (a, b)) to the context of the type signature for `bar'' or add an instance declaration for (C (a, b)) In the expression: bar In the definition of `bar'': bar' = bar

So, we have this problem as soon as we have flexible contexts and/or MPTCs, independent of TFs and FDs.

Manuel

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

type family Id a

type instance Id Int = Int

foo :: Id a -> Id a foo = id n

foo' :: Id a -> Id a foo' = foo

type function notation is slightly misleading, as it presents qualified polymorphic types in a form usually reserved for unqualified polymorphic types. rewriting foo's type helped me to see the ambiguity that others have pointed out: foo :: r ~ Id a => r -> r there's nowhere to get the 'a' from. so unless 'Id' itself is fully polymorphic in 'a' (Id a = a, Id a = Int, ..), 'foo' can't really be used. for each type variable, there needs to be at least one position where it is not used as a type family parameter. it might be useful to issue an ambiguity warning for such types? perhaps, with closed type families, one might be able to reason backwards (is there a unique 'a' such that 'Id a ~ Int'?), as with bidirectional FDs. but if you want to flatten all 'Maybe'-nests, even that direction isn't unique.

The type checking problem for foo' boils down to verifying the formula

forall a. exists b. Id a ~ Id b

naively, i'd have expected to run into this instead/first: (forall a. Id a -> Id a) ~ (forall b. Id b -> Id b) which ought to be true modulo alpha conversion, without guesses, making 'foo'' as valid/useless as 'foo' itself. where am i going wrong? claus ps. i find these examples and discussions helpful, if often initially puzzling - they help to clear up weak spots in the practice of type family use, understanding, and implementation, thereby improving all while making families more familiar!-)

Claus Reinke:

...

type family Id a type instance Id Int = Int

foo :: Id a -> Id a foo = id n foo' :: Id a -> Id a foo' = foo

type function notation is slightly misleading, as it presents qualified polymorphic types in a form usually reserved for unqualified polymorphic types.

rewriting foo's type helped me to see the ambiguity that others have pointed out:

foo :: r ~ Id a => r -> r

there's nowhere to get the 'a' from. so unless 'Id' itself is fully polymorphic in 'a' (Id a = a, Id a = Int, ..), 'foo' can't really be used. for each type variable, there needs to be at least one position where it is not used as a type family parameter.

Yes. It is generally so that the introduction of indexed types (ie, all of GADTs, data type families, or synonym families) means that a type with a parameter is not necessarily parametric.

it might be useful to issue an ambiguity warning for such types?

The problem is that testing for ambiguity is, in general, difficult. Whether a context is ambiguous depends for example on the currently visible class instances. As a result, a signature that is ambiguous in a module M, may be fine in a module N that imports M. However, I think what should be easier is to improve the error messages given when a function with an ambiguous signature is used. For example, if the error message in the definition of foo' would have included a hint saying that the definition is illegal because its right hand side contains the use of a function with an ambiguous signature, then Ganesh may have had an easier time seeing what's happening.

ps. i find these examples and discussions helpful, if often initially puzzling - they help to clear up weak spots in the practice of type family use, understanding, and implementation, thereby improving all while making families more familiar!-)

Absolutely! Manuel