Attached file `contextBug.lhs`

(download).

Corrected ticket

Attached file `condBug.lhs`

(download).

Attached file `typeBug.lhs`

(download).

Code for the bug report

The following should fail with an appropriate error message.

I discovered this by accident when I changed the definition of type 'U' and forgot to remove 'deriving Functor'.

```
> {-# LANGUAGE TypeFamilies, DeriveFunctor #-}
> data U a = U (G a) deriving Functor
>
> class A a where
> type G a
```

Trac field | Value |
---|---|

Version | 7.2.1 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |

I am sorry. I sent the wrong code version. There should be no [a] in there. This was the attempt mentionned at the end of the comment.

When testing again, I also surprised to see that okInBoth' in fact compiles in 7.0.2 only. I don't know what happened here. So I am renaming it to okIn702, and pasting an updated description below :

GHC 7.0.2 rejects programs which 7.0.1 accepts, and vice-versa

A passed context is not used, and the compiler (expectedly) fails to deduce an instance. Patching the code so that it works again is not difficult. Some type annotations can do the trick. So this is not a critical issue but it is a bit surprising.

I have simplified my code as much as possible so that it still shows the error in 7.0.2 (okIn701). I have included two further simplifications. One produces no error in both versions (okInBoth) and the other produces an error in 7.0.1 (okIn702).

The code also compiles if we remove the instance declaration for class B. In that case the type of a in okIn701 can be infered, and the context for that type is provided.

I have seen the following comment by dimitris in ticket #4981 (closed), which seems related. "I know why GHC is not picking the given up: it has to do with the fact that we have not saturated all possible equalities before we look for instances, but luckily this is something Simon and I are planning to fix pretty soon." Ticket #4981 (closed) seems to be an issue with 7.0.1. In the initial ticket text I though this was a regression with 7.0.2, but in some cases 7.0.2 is better than 7.0.1 (okIn702).

The diagnosis of ticket #3018 (closed) may be applicable to the code here: we may be asking too much of the compiler. As an additional simplification attempt, I have added function fromTicket3018, but it compiles fine with 7.0.1 and 7.0.2.

Also if the instance for 'B' is restricted to '[a]' (we can then remove the UndecidableInstances extension), and the type 'a' is replaced by '[a]' in 'okIn701', then it compiles fine. Are instances that match everything applied more eagerly ? If so then this compilatin problem should be quite rare.

```
> {-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, FlexibleContexts #-}
> class A a
> class B a where b :: a -> ()
> instance A a => B a where b = undefined
> newtype Y a = Y (a -> ())
> okIn701 :: B a => Y a
> okIn701 = wrap $ const () . b
> okIn702 :: B a => Y a
> okIn702 = wrap $ b
> okInBoth :: B a => Y a
> okInBoth = Y $ const () . b
> class Wrapper a where
> type Wrapped a
> wrap :: Wrapped a -> a
> instance Wrapper (Y a) where
> type Wrapped (Y a) = a -> ()
> wrap = Y
> fromTicket3018 :: Eq [a] => a -> ()
> fromTicket3018 x = let {g :: Int -> Int; g = [x]==[x] `seq` id} in ()
> main = undefined
```

GHC 7.0.2 rejects programs which 7.0.1 accepts.

A passed context is not used, and the compiler (expectedly) fails to deduce an instance. Patching the code so that it works again is not difficult. Some type annotations can do the trick. So this is not a critical issue but it is a bit surprising.

I have simplified my code as much as possible so that it still shows the error in 7.0.2 (okIn701). I have included two further simplifications which produce no error : okInBoth and okInBoth'. I see why okInBoth is more simple (it side steps a type function), but I do not see why okInBoth' would avoid the problem.

The code also compiles if we remove the instance declaration for class B. In that case the type of a in okIn701 can be infered, and the context for that type is provided.

I have seen the following comment by dimitris in ticket #4981, which seems related. "I know why GHC is not picking the given up: it has to do with the fact that we have not saturated all possible equalities before we look for instances, but luckily this is something Simon and I are planning to fix pretty soon." Ticket #4981 seems to be an issue with 7.0.1. Here we see an apparent regression with 7.0.2, so I thought I would bring it up in case it is an unexpected change in behavior.

The diagnosis of ticket #3018 may be applicable to the code here: we may be asking too much of the compiler. As an additional simplification attempt, I have added function fromTicket3018, but it compiles fine with 7.0.1 and 7.0.2.

Also if the instance for 'B' is restricted to '[a]' (we can then remove the UndecidableInstances extension), and the type 'a' is replaced by '[a]' in 'okIn701', then it compiles fine. Are instances that match everything applied more eagerly ? If so then this compilatin problem should be quite rare.

```
> {-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, FlexibleContexts #-}
> class A a
> class B a where b :: a -> ()
> instance A a => B [a] where b = undefined
> newtype Y a = Y (a -> ())
> okIn701 :: B [a] => Y [a]
> okIn701 = wrap $ const () . b
> okInBoth' :: B a => Y a
> okInBoth' = wrap $ b
> okInBoth :: B a => Y a
> okInBoth = Y $ const () . b
> class Wrapper a where
> type Wrapped a
> wrap :: Wrapped a -> a
> instance Wrapper (Y a) where
> type Wrapped (Y a) = a -> ()
> wrap = Y
> fromTicket3018 :: Eq [a] => a -> ()
> fromTicket3018 x = let {g :: Int -> Int; g = [x]==[x] `seq` id} in ()
> main = undefined
```

Trac field | Value |
---|---|

Version | 7.0.2 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |

The following produces a type error with ghc-7.1.20110126. No error is reported by ghc-7.0.1.

```
condBug.lhs:48:29:
Could not deduce (a ~ CondV c a (f a))
from the context (TBool c, Functor f)
bound by the type signature for
condMap :: (TBool c, Functor f) =>
(a -> b) -> Cond c f a -> Cond c f b
at condBug.lhs:48:3-40
or from (c ~ TFalse)
bound by a type expected by the context:
c ~ TFalse => CondV c a (f a) -> b
at condBug.lhs:48:24-40
`a' is a rigid type variable bound by
the type signature for
condMap :: (TBool c, Functor f) =>
(a -> b) -> Cond c f a -> Cond c f b
at condBug.lhs:48:3
Expected type: CondV c a (f a) -> b
Actual type: a -> b
In the first argument of `cond', namely `g'
In the expression: cond g (fmap g) n
```

```
> {-# LANGUAGE TypeFamilies, Rank2Types, ScopedTypeVariables #-}
> import Control.Applicative
> data TFalse
> data TTrue
> data Tagged b a = Tagged {at :: a}
> type At b = forall a. Tagged b a -> a
> class TBool b where onTBool :: (b ~ TFalse => c) -> (b ~ TTrue => c) -> Tagged b c
> instance TBool TFalse where onTBool f _ = Tagged $ f
> instance TBool TTrue where onTBool _ t = Tagged $ t
> type family CondV c f t
> type instance CondV TFalse f t = f
> type instance CondV TTrue f t = t
> newtype Cond c f a = Cond {getCond :: CondV c a (f a)}
> cond :: forall c f a g. (TBool c, Functor g) => (c ~ TFalse => g a) -> (c ~ TTrue => g (f a)) -> g (Cond c f a)
> cond f t = (at :: At c) $ onTBool (fmap Cond f) (fmap Cond t)
> condMap :: (TBool c, Functor f) => (a -> b) -> Cond c f a -> Cond c f b
> condMap g (Cond n) = cond g (fmap g) n
> main = undefined
```

The type error seems inappropriate. Given the defintion of 'CondV', and the 'c ~ TFalse' available form the context, shouldn't the compiler see that 'CondV c a (f a) ~ a' ?

Trac field | Value |
---|---|

Version | 7.1 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler (Type checker) |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |

Trac field | Value |
---|---|

Version | 6.12.1 → 7.1 |

The following throws ghc (and ghci) in a loop (ghc-7.0.0.20100925 for i386-unknown-mingw32) and it eventually aborts with "ghc.exe: out of memory".

```
> {-# LANGUAGE TypeFamilies, Rank2Types, FlexibleContexts #-}
> type family T a
> t2 :: forall a. ((T a ~ a) => a) -> a
> t2 = t
> t :: forall a. ((T a ~ a) => a) -> a
> t = undefined
```

Using ghc 6.12.1 we do not get a loop, but a puzzling error:

typeBug.lhs:9:7:

Couldn't match expected type `(T a ~ a) => a' against inferred type `

(T a ~ a) => a'

Expected type: (T a ~ a) => a

Inferred type: (T a ~ a) => a

In the expression: t

In the definition of `t2': t2 = t

I presume that the non-injectivity of type family T triggers the problem however the following produces no errors in either version of the compiler.

```
> ok2 :: forall a. T a -> a
> ok2 = ok
> ok :: forall a. T a -> a
> ok = undefined
```

Trac field | Value |
---|---|

Version | 6.12.1 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler (Type checker) |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |