## #14203 closed bug (invalid)

# GHC-inferred type signature doesn't actually typecheck

Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler (Type checker) | Version: | 8.2.1 |

Keywords: | TypeInType, TypeFamilies | Cc: | |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | GHC rejects valid program | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description

This code typechecks:

{-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 data family Sing :: k -> * data Sigma (a :: *) :: (a ~> *) -> * where MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a). Sing x -> Apply p x -> Sigma a p data instance Sing (z :: Sigma a p) where SMkSigma :: Sing sx -> Sing px -> Sing (MkSigma sx px)

I was curious to know what the full type signature of `SMkSigma`

was, so I asked GHCi what the inferred type is:

λ> :i SMkSigma data instance Sing z where SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x). (Sing sx) -> (Sing px) -> Sing ('MkSigma sx px)

I attempted to incorporate this newfound knowledge into the program:

{-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 data family Sing :: k -> * data Sigma (a :: *) :: (a ~> *) -> * where MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a). Sing x -> Apply p x -> Sigma a p data instance Sing (z :: Sigma a p) where SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x). Sing sx -> Sing px -> Sing (MkSigma sx px)

But to my surprise, adding this inferred type signature causes the program to no longer typecheck!

GHCi, version 8.3.20170907: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:23:31: error: • Expected kind ‘Apply p0 x’, but ‘px’ has kind ‘Apply p1 x’ • In the first argument of ‘Sing’, namely ‘px’ In the type ‘Sing px’ In the definition of data constructor ‘SMkSigma’ | 23 | Sing sx -> Sing px -> Sing (MkSigma sx px) | ^^

I'm showing the output of GHC HEAD here, but this bug can be reproduced all the way back to GHC 8.0.1.

### Change History (19)

### comment:1 Changed 3 months ago by

### comment:2 Changed 3 months ago by

The original programs should be rejected, I think. Looking at your simpler example, the declaration for `Foo`

should be rejected as ambiguous. There's no way to tell from `z`

what `a`

, `x`

, or `p`

should be. When I continue my bug sweep, I'll take a look at this.

### comment:3 Changed 3 months ago by

I can accept that the second program (with `MkBar`

) would be ambiguous, but I don't understand what is wrong with the original program (with `SMkSigma`

), especially the form when an explicit `forall`

.

### comment:4 Changed 2 months ago by

The type of `SMkSigma`

is also ambiguous. There's no way to infer `p`

from the visible arguments.

### comment:5 Changed 2 months ago by

Huh, that's interesting... how do you resolve such an ambiguity, then? Normally, my approach is to add proxies until the ambiguity is resolved, such as what I tried below:

{-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind import Data.Proxy data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 data family Sing :: k -> * data Sigma (a :: *) :: (a ~> *) -> * where MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a). Sing x -> Apply p x -> Sigma a p data instance Sing (z :: Sigma a p) where SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x). Proxy a -> Proxy p -> Proxy x -> Sing sx -> Sing px -> Sing (MkSigma sx px)

But that still results in the same error. Adding `AllowAmbiguousTypes`

doesn't help either.

### comment:6 Changed 3 weeks ago by

Actually, it's not just limited to datatypes: the same effect can be observed in this program:

{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where type family F a data Foo (z :: F a) bar :: forall a (z :: F a). Foo z -> Int bar _ = 42

$ /opt/ghc/8.2.1/bin/ghci Bug.hs GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/ryanglscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:10:33: error: • Expected kind ‘F a0’, but ‘z’ has kind ‘F a’ • In the first argument of ‘Foo’, namely ‘z’ In the type signature: bar :: forall a (z :: F a). Foo z -> Int | 10 | bar :: forall a (z :: F a). Foo z -> Int | ^

Here, I would expect `AllowAmbiguousTypes`

to squash the error message about the ambiguous variable `a0`

in `F a0`

, but that doesn't happen.

### comment:7 follow-up: 8 Changed 3 weeks ago by

In comment:6 we have

Foo :: forall a. F a -> *

That's an ambiguous kind! Just like for a function

foo :: forall k. F k -> Int

is ambiguous. So all uses of `Foo`

will give rise to ambiguity. But alas we do not check for ambiguous kinds.

Instead we see a "call" of `Foo`

in the type signature

bar :: forall a (z :: F a). Foo z -> Int

At the use of `Foo`

we intantiate `k`

to `kappa`

and check that `F kappa`

is equal o the kind of `z`

namely `F a`

. So for the type to be well-kinded we need `F kappa ~ F a`

. But we have no way to prove that (unless `F`

is injective). And that's the error.

TL;DR: it's `Foo`

that should be rejected as having an ambiguous kind.

(I have not studied the oroginal Description; just assuming that comment:6 embodies the essence.)

### comment:8 Changed 3 weeks ago by

I'm well aware of the fact that this is an ambiguous definition. But the point that I'm making (that no one has addressed yet) is that `AllowAmbiguousTypes`

should allow GHC to accept such a definition!

Replying to simonpj:

But alas we do not check for ambiguous kinds.

If we don't do this currently, then we should! There are many programs that I can't write because of this restriction.

### comment:9 follow-up: 10 Changed 3 weeks ago by

But the point that I'm making (that no one has addressed yet) is that AllowAmbiguousTypes should allow GHC to accept such a definition!

I don't agree. It's the definition of `Foo`

that has an ambiguous kind. ThE type signature for `bar`

is entirely innocent. To see this more clearly try

bar :: forall a (z :: F a). Foo z -> Proxy z -> Int

Nothing ambiguous about that. But simply kind-checking the type signature fails because `Foo`

's kind is ambiguous.

If we don't do this currently, then we should! There are many programs that I can't write because of this restriction. ]

What is "this"? Rejecting the definition of `Foo`

(which would be the effect of checking `Foo`

's kind for ambiguity) would not typecheck more programs!

### comment:10 Changed 3 weeks ago by

Replying to simonpj:

I don't agree. It's the definition of

`Foo`

that has an ambiguous kind.

OK, sure. The point is—there's *some* definition in this program with an ambiguous kind, and `AllowAmbiguousTypes`

is not convincing GHC to accept it. If the burden of ambiguity proof needs to be shifted to `Foo`

instead, that's fine.

What is "this"? Rejecting the definition of

`Foo`

(which would be the effect of checking`Foo`

's kind for ambiguity) would not typecheck more programs!

The point is that I *want* GHC to accept `Foo`

(and `bar`

). The mechanism by which I normally do so (`AllowAmbiguousTypes`

) is failing me here.

### comment:11 Changed 3 weeks ago by

I don't see how you want GHC to accept `bar`

. Let's take this slowly.

```
`
type family F a
```

```
`
```

So far, so good.

```
`
data Foo (z :: F a)
```

```
`
```

As Simon points out, `Foo`

has an ambiguous kind `forall (a :: Type). F a -> Type`

. There's no way to infer the choice of `a`

from a usage of `Foo`

. GHC does not check for ambiguous kinds (it should, I agree), so this definition is accepted with or without `AllowAmbiguousTypes`

. Regardless, you've specified `AllowAmbiguousTypes`

, so accepting this conforms to your stated desires.

```
`
bar :: forall a (z :: F a). Foo z -> Int
```

```
`
```

Now we're in deep trouble. This type mentions `Foo z`

. Accordingly, GHC must infer the invisible kind parameter to `Foo`

. (You might say "Well, obviously it should be `a`

!", but that would be assuming `F`

is injective.) So GHC rejects this type signature, as it doesn't know what the invisible kind parameter to `Foo`

should be. Note that this is *not* the normal ambiguity check that `AllowAmbiguousTypes`

disables. This type has an ambiguous type variable; the type itself is not ambiguous.

### comment:12 Changed 3 weeks ago by

OK. So what you're saying is that:

bar :: forall a (z :: F a). Foo z -> Int

Should be rejected as an ambiguous *occurrence* site (which `AllowAmbiguousTypes`

does not permit) rather than an ambiguous *definition* site (which `AllowAmbiguousType`

*does* permit)?

I could buy that, although I'm a bit miffed that there doesn't appear to be a satisfying way to resolve the ambiguity. In an ideal world, you could say:

bar :: forall (a :: k) (z :: F @k a). Foo z -> Int

But there's no visible kind application. In a fit of rage, I even tried giving kind signatures to *everything*:

{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where type family F (a :: k) data Foo (z :: F (a :: k)) bar :: forall (a :: k) (z :: F (a :: k)). Foo (z :: F (a :: k)) -> Int bar _ = 42

But that still produces the same error. So how am I supposed to proceed from here?

### comment:13 Changed 3 weeks ago by

You're not. Don't write a type with an ambiguous kind. :)

Alternatively, and even better, implement visible kind application.

### comment:14 Changed 3 weeks ago by

OK, I found out how to do this. The trick is to make the kind of `a`

in `F`

visible:

{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where type family F a data Foo a (z :: F a) bar :: forall a (z :: F a). Foo a z -> Int bar _ = 42

A similar trick works for the program in comment:1:

{-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 data Foo p x (z :: Apply (p :: a ~> *) (x :: a)) data Bar where MkBar :: forall a (p :: TyFun a * -> *) (x :: a) (z :: Apply p x). Foo p x z -> Bar

Alas, this trick doesn't scale very well to the original program, since you'd need to give `p`

as a visible argument to `Sing px`

somehow. (It's not clear to me if even visible kind application would fix this problem.)

### comment:15 Changed 3 weeks ago by

Should be rejected as an ambiguous occurrence site (which AllowAmbiguousTypes does not permit) rather than an ambiguous definition site (which AllowAmbiguousType does permit)?

Yes. Precisely like this case:

{-# LANGUAGE AllowAmbiguousTypes #-} f :: F a -> Int -- Ambiguous, but allowed because of the pragma f = e boogle :: F b -> Int boogle v = f v

GHC instantiates `F`

at `alpha`

and then complains it can't equate `F b ~ F alpha`

. Visible type application is the solution.

The only thing happening in this ticket is that this very same pattern is manifesting at the type level instead of the term level. Nothing more!

### comment:16 Changed 3 weeks ago by

OK. So after these musings about `AllowAmbiguousTypes`

, kind ambiguities, and visible kind application, I've lost track if there's actually any concrete GHC bug that's manifesting in the original program. Can this be closed, or is there something left to be done?

### comment:17 Changed 3 weeks ago by

I think that comment:6 is not a bug. I have not analysed the more complex examples. If they are the same, let's indeed close.

### comment:18 Changed 3 weeks ago by

Resolution: | → invalid |
---|---|

Status: | new → closed |

### comment:19 Changed 3 weeks ago by

I've just created #14419 to request an ambiguity check on kinds, which may have helped Ryan not to get caught in this trap.

**Note:**See TracTickets for help on using tickets.

Here's a slightly simpler example that doesn't use

`singletons`

. This compiles:And if you ask GHCi for the type of

`MkBar`

, you get:But if you try using that:

It fails: