On 07/04/2009, Ryan Ingram wrote:

On Mon, Apr 6, 2009 at 2:36 PM, Peter Berry wrote:

...

As I understand it, the type checker's thought process should be along these lines:

1) the type signature dictates that x has type Memo d a. 2) appl has type Memo d1 a -> d1 -> a for some d1. 3) we apply appl to x, so Memo d1 a = Memo d a. unify d = d1

This isn't true, though, and for similar reasons why you can't declare a generic "instance Fun d => Functor (Memo d)". Type synonyms are not injective; you can have two instances that point at the same type:

Doh! I'm too used to interpreting words like "Memo" with an initial capital as constructors, which are injective, when it's really a function, which need not be.

You can use a data family instead, and then you get the property you want; if you make Memo a data family, then Memo d1 = Memo d2 does indeed give you d1 = d2.

I'm now using Data.MemoTrie, which indeed uses data families, instead of a home-brewed solution, and now GHC accepts the type signature. In fact, it already has a Functor instance, so funmap is redundant. -- Peter Berry Please avoid sending me Word or PowerPoint attachments. See http://www.gnu.org/philosophy/no-word-attachments.html

On Mon, Apr 6, 2009 at 7:39 PM, Manuel M T Chakravarty

wrote:

Peter Berry:

...

3) we apply appl to x, so Memo d1 a = Memo d a. unify d = d1

But for some reason, step 3 fails.

Step 3 is invalid - cf, < http://www.haskell.org/pipermail/haskell-cafe/2009-April/059196.html>.

More generally, the signature of memo_fmap is ambiguous, and hence, correctly rejected. We need to improve the error message, though. Here is a previous discussion of the subject:

http://www.mail-archive.com/haskell-cafe@haskell.org/msg39673.html

Manuel

The thing that confuses me about this case is how, if the type sig on memo_fmap is omitted, ghci has no problem with it, and even gives it the type that it rejected: ------------------------------------------------ {-# LANGUAGE TypeFamilies #-} class Fun d where type Memo d :: * -> * abst :: (d -> a) -> Memo d a appl :: Memo d a -> (d -> a) memo_fmap f x = abst (f . appl x) -- [m@monire a]$ ghci -ignore-dot-ghci -- GHCi, version 6.10.1: http://www.haskell.org/ghc/ :? for help -- -- Prelude> :l ./Memo.hs -- [1 of 1] Compiling Main ( Memo.hs, interpreted ) -- Ok, modules loaded: Main. -- -- *Main> :t memo_fmap -- memo_fmap :: (Fun d) => (a -> c) -> Memo d a -> Memo d c -- copy/paste the :t sig memo_fmap_sig :: (Fun d) => (a -> c) -> Memo d a -> Memo d c memo_fmap_sig f x = abst (f . appl x) -- and, -- *Main> :r -- [1 of 1] Compiling Main ( Memo.hs, interpreted ) -- -- Memo.hs:26:35: -- Couldn't match expected type `Memo d' -- against inferred type `Memo d1' -- In the first argument of `appl', namely `x' -- In the second argument of `(.)', namely `appl x' -- In the first argument of `abst', namely `(f . appl x)' -- Failed, modules loaded: none. ------------------------------------------------ Matt

Basically, type checking proceeds in one of two modes: inferring or checking. The former is when there is no signature is given; the latter, if there is a user-supplied signature. GHC can infer ambiguous signatures, but it cannot check them. This is of course very confusing and we need to fix this (by preventing GHC from inferring ambiguous signatures). The issue is also discussed in the mailing list thread I cited in my previous reply.

As the error message demonstrates, the inferred type is not correctly represented - GHC doesn't really infer an ambiguous type, it infers a type with a specific idea of what the type variable should match. Representing that as an unconstrained forall-ed type variable just doesn't seem accurate (as the unconstrained type variable won't match the internal type variable) and it is this misrepresentation of the inferred type that leads to the ambiguity. Here is a variation to make this point clearer: {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE TypeFamilies, ScopedTypeVariables #-} class Fun d where type Memo d :: * -> * abst :: (d -> a) -> Memo d a appl :: Memo d a -> (d -> a) f = abst . appl -- f' :: forall d a. (Fun d) => Memo d a -> Memo d a f' = abst . (id :: (d->a)->(d->a)) . appl There is a perfectly valid type signature for f', as given in comment, but GHCi gives an incorrect one (the same as for f): *Main> :browse Main class Fun d where abst :: (d -> a) -> Memo d a appl :: Memo d a -> d -> a f :: (Fun d) => Memo d a -> Memo d a f' :: (Fun d) => Memo d a -> Memo d a What I suspect is that GHCi does infer the correct type, with constrained 'd', but prints it incorrectly (no forall to indicate the use of scoped variable). Perhaps GHCi should always indicate in its type output which type variables have been unified with type variables that no longer occur in the output type (here the local 'd'). If ScopedTypeVariables are enabled, that might be done via explicit forall, if the internal type variable occurs in the source file (as for f' here). Otherwise, one might use type equalities. In other words, I'd expect :browse output more like this: f :: forall a d. (Fun d, d~_d) => Memo d a -> Memo d a f' :: forall a d. (Fun d) => Memo d a -> Memo d a making the first signature obviously ambiguous, and the second signature simply valid. Claus

| Here is a variation to make this point clearer: | | {-# LANGUAGE NoMonomorphismRestriction #-} | {-# LANGUAGE TypeFamilies, ScopedTypeVariables #-} | | class Fun d where | type Memo d :: * -> * | abst :: (d -> a) -> Memo d a | appl :: Memo d a -> (d -> a) | | f = abst . appl | | -- f' :: forall d a. (Fun d) => Memo d a -> Memo d a | f' = abst . (id :: (d->a)->(d->a)) . appl | | There is a perfectly valid type signature for f', as given in | comment, but GHCi gives an incorrect one (the same as for f): | | *Main> :browse Main | class Fun d where | abst :: (d -> a) -> Memo d a | appl :: Memo d a -> d -> a | f :: (Fun d) => Memo d a -> Memo d a | f' :: (Fun d) => Memo d a -> Memo d a

I'm missing something here. Those types are identical to the one given in your type signature for f' above, save that the forall is suppressed (because you are allowed to omit it, and GHC generally does when printing types).

Not with ScopedTypeVariables, though, where explicit foralls have been given an additional significance. Uncommenting the f' signature works, while dropping the 'forall d a' from it fails with the usual match failure due to ambiguity "Couldn't match expected type `Memo d1' against inferred type `Memo d'".

I must be missing the point.

The point was in the part you didn't quote: |In other words, I'd expect :browse output more like this: | |f :: forall a d. (Fun d, d~_d) => Memo d a -> Memo d a |f' :: forall a d. (Fun d) => Memo d a -> Memo d a | |making the first signature obviously ambiguous, and the |second signature simply valid. Again, the validity of the second signature depends on ScopedTypeVariables - without that, both f and f' should get a signature similar to the first one (or some other notation that implies that 'd' isn't freely quantified, but must match a non-accessible '_d'). Claus

|Oh now i see what you mean: consider | f' = abst . (id :: (d->a)->(d->a)) . appl |which GHC understands to mean | f' = abst . (id :: forall d a. (d->a)->(d->a)) . appl | |GHC infers the type | f' :: (Fun d) => Memo d a -> Memo d a |Now you are saying that GHC *could* have figured out that if it added the signature | f' :: forall d a. (Fun d) => Memo d a -> Memo d a |thereby *changing* the scoping of d,a in the buried signature for 'id', doing so would not change whether f' was |typeable or not. Well maybe, but that is way beyond what I have any current plans to do. Indeed!-) I didn't mean to suggest this as a course of action, it was just a way of representing the internal type inference intermediates at source level. Another aspect I would not like about this approach is that renamings of bound type variables would no longer be meaning- preserving (because the signature would be interpreted in the context of the source-code it belongs to) - not good. But the core part of my suggestion (which this example was meant to help explain) remains attractive, at least to me: somewhere during type inference, GHC *does* unify the *apparently free* 'd' with an internal type variable (lets call it 'd1, as in the type error message) that has no explicit counterpart in source code or type signature, so the inferred type should not be f' :: forall d. (Fun d) => Memo d a -> Memo d a -- (1) but rather f' :: forall d. (Fun d,d~d1) => Memo d a -> Memo d a -- (2) That way, the internal dependency would be made explicit in the printed representation of the inferred type signature, and the unknown 'd1' would appear explicitly in the inferred type, not just in the error message (the explicit foralls are needed here to make it clear that 'd1' and by implication, 'd', *cannot* be freely generalized - 'd' is qualified by the equation with the unknown 'd1'). To me, (2) makes more sense as an inferred type for f' than (1), especially as it represents an obviously unusable type signature (we don't know what 'd1' is, and we can't just unify it with anything), whereas (1) suggests a useable type signature, but one that will fail when used: Couldn't match expected type `Memo d1' against inferred type `Memo d'. All I'm suggesting is that the type *printed* by GHCi does not really represent the type *inferred* by GHCi (or else there should not be any attempt to match the *free* 'd' against some unknown 'd1', as the error message says), and that there might be ways to make the discrepancy explicit, by printing the inferred type differently. Claus

| But the core part of my suggestion (which this example was meant | to help explain) remains attractive, at least to me: somewhere during | type inference, GHC *does* unify the *apparently free* 'd' with an | internal type variable (lets call it 'd1, as in the type error message)

You are speculating about the *algorithm*.

There is no need to reason about the algorithm, only about its observable results ('d1' appeared in the error message, but not in the inferred type). But I've finally figured out what had me confused - sadly something that has come up before, I just had forgotten to apply it here. First, the code again: {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE TypeFamilies #-} class Fun d where type Memo d :: * -> * abst :: (d -> a) -> Memo d a appl :: Memo d a -> (d -> a) -- f :: (Fun d) => Memo d a -> Memo d a -- (1) f = abst . appl (1) is the type inferred by GHCi. If we uncomment it, we get this error: D:\home\Haskell\tmp\desktop\types.hs:11:11: Couldn't match expected type `Memo d1' against inferred type `Memo d' In the second argument of `(.)', namely `appl' In the expression: abst . appl In the definition of `f': f = abst . appl My _erroneous_ reasoning was that some unknown 'd1' was being unified with the 'd' from the signature. So I wanted that 'd1' to be represented in the signature inferred by GHCi. Of course, the error message really says something quite different, and if I had recalled that 'Memo' is a type synonym, I would have noticed that. If GHC ever provides an option to bracket fully applied type synonyms, I'd probably switch it on by default. (what one actually wants is a way to distinguish type-level general functions from type-level constructors that can be decomposed during unification, similar to what Haskell does with capitalization at the expression level, to distinguish general functions from constructors that can be decomposed during matching). With such an option, the inferred type would look like this (er, hi Conor): f :: (Fun d) => {Memo d} a -> {Memo d} a The first parameter of 'Memo' is not directly available for unification, so this signature is ambiguous as it stands, as you tried to point out (with no way to pin down 'd', 'Memo d' can never unify with anything other than itself, identically). Apart from bracketing fully applied type synonyms, the error message could be improved by providing the missing bit of information about 'Memo': D:\home\Haskell\tmp\desktop\types.hs:11:11: Couldn't match expected type `Memo d1' against inferred type `Memo d' (type Memo d :: * -> *) In the second argument of `(.)', namely `appl' In the expression: abst . appl In the definition of `f': f = abst . appl Sorry about letting myself get confused again by this known issue. Claus PS. I thought I'd try this alternative signature, to make the ambiguity explicit: f :: (Memo d~md,Fun d) => md a -> md a -- (2) but the error message is even less helpful: D:\home\Haskell\tmp\desktop\types.hs:11:11: Couldn't match expected type `Memo d' against inferred type `md' `md' is a rigid type variable bound by the type signature for `f' at D:\home\Haskell\tmp\desktop\types.hs:10:14 In the second argument of `(.)', namely `appl' In the expression: abst . appl In the definition of `f': f = abst . appl Shouldn't the inferred type still be 'Memo d1'? Why is part of the _declared_ type "expected" ('Memo d'), the other "inferred" ('md')? Could GHC perhaps be more detailed about 'expected', 'inferred', and 'declared', and use these terms from a user perspective? Even in the original error message, shouldn't 'expected' and 'inferred' be the other way round? And if we add the missing contexts for the types mentioned in the message, the error message could really be: D:\home\Haskell\tmp\desktop\types.hs:11:11: Couldn't match inferred type `Memo d1' (f :: (Fun d1) => {Memo d1} a -> {Memo d1} a) against declared type `Memo d' (f :: (Fun d) => {Memo d} a -> {Memo d} a) (type {Memo d} :: * -> *) In the second argument of `(.)', namely `appl' In the expression: abst . appl In the definition of `f': f = abst . appl Perhaps then I would have seen what was going on?-)

Simon Peyton-Jones wrote:

NoMatchErr.hs:20:11: Couldn't match expected type `Memo d' against inferred type `Memo d1' NB: `Memo' is a (non-injective) type function In the second argument of `(.)', namely `appl' In the expression: abst . appl In the definition of `f': f = abst . appl

(Rather than give its kind, I thought it was better to focus on the reason for the mis-match, namely the non-injectivity.)

I'd suggest "is a type function and thus may not be injective" or similar, otherwise people will think that type functions which are injective according to the instances they've defined would be ok. Cheers, Ganesh =============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ===============================================================================

On Wed, May 27, 2009 at 9:59 PM, Bulat Ziganshin wrote:

Hello Simon,

Wednesday, May 27, 2009, 11:42:22 PM, you wrote:

while we are here - i always had problems understanding what is inferred and what is expected type. may be problem is just that i'm not native speaker

are other, especially beginners, had the same problem?

The inferred type of e is the type that the compiler thinks e has. The expected type is the type it *should* have, given its context. Consider: f :: Int -> Int then the expression (f True) has a type error: Couldn't match expected type `Int' against inferred type `Bool' In the first argument of `f', namely `True' GHC is saying the first argument of f *should* be an Int, but it seems to be a Bool. As to whether it's confusing, I sometimes have to read these messages a few times (sometimes it's unclear which expression is being referred to, or why GHC thinks that the expression has a certain type), but the words themselves are clear in their meaning to me. HTH, Max

On Wed, May 27, 2009 at 10:28 PM, Bulat Ziganshin wrote:

can you recall early times of your work with GHC? i think that these words are non-obvious for novices. finally it becomes part of your instincts as anything else often used. but it can be learning barrier. overall, hard-to-understand error messages was elected as one of 3 most important GHC problems in the survey conducted several years ago

I don't remember having any trouble, but that was a few years ago, and type errors are confusing generally. I think that the main difficulty with type errors is not the error *messages*, but I'm sure there is room for improvement. Do you have any ideas? --Max

Bulat Ziganshin wrote:

Error: type of x is Integer while type of read argument should be String

The problem with this is that the compiler can't know whether or not the type of arguments to read should be a String, as someone could have messed up read's signature. Granted, you have to have a knack for semantic bickering to not just glance over the imprecision. -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited.

Bulat Ziganshin wrote:

Hello Achim,

Thursday, May 28, 2009, 1:34:55 AM, you wrote:

...

...

Error: type of x is Integer while type of read argument should be String

The problem with this is that the compiler can't know whether or not the type of arguments to read should be a String, as someone could have messed up read's signature.

i don't understood what you mean, can you give an example?

Error : type of x is String while the type of an argument to read should be Integer , given that, somewhere, you have read :: Integer -> a , which is, of course, wrong, and that's the point. -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited.

Hello Henning, Thursday, May 28, 2009, 2:06:36 AM, you wrote: Prelude>> let a = 'a'; b = "b" in a==b

<interactive>:1:27: Couldn't match expected type `Char' against inferred type `[Char]' ....

Is the type of 'a' wrong or that of 'b'?

it is not important, well, at least we can live with it. Compiler should say: First argument of == should be of type String while a is of type Char and then it's user's problem to decide whether he need to fix call or argument. only some interactive IDE may allow user to select term to fix and then give him message tuned to this exact term -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

On Mon, Apr 6, 2009 at 7:39 PM, Manuel M T Chakravarty wrote:

Peter Berry:

...

3) we apply appl to x, so Memo d1 a = Memo d a. unify d = d1

But for some reason, step 3 fails.

Step 3 is invalid - cf, http://www.haskell.org/pipermail/haskell-cafe/2009-April/059196.html.

More generally, the signature of memo_fmap is ambiguous, and hence, correctly rejected. We need to improve the error message, though. Here is a previous discussion of the subject:

http://www.mail-archive.com/haskell-cafe@haskell.org/msg39673.html

Aha! Very informative, thanks. On 07/04/2009, Manuel M T Chakravarty wrote:

Matt Morrow:

...

The thing that confuses me about this case is how, if the type sig on memo_fmap is omitted, ghci has no problem with it, and even gives it the type that it rejected:

Basically, type checking proceeds in one of two modes: inferring or checking. The former is when there is no signature is given; the latter, if there is a user-supplied signature. GHC can infer ambiguous signatures, but it cannot check them. This is of course very confusing and we need to fix this (by preventing GHC from inferring ambiguous signatures). The issue is also discussed in the mailing list thread I cited in my previous reply.

I see. So GHC is wrong to accept memo_fmap? -- Peter Berry Please avoid sending me Word or PowerPoint attachments. See http://www.gnu.org/philosophy/no-word-attachments.html