Opened 2 weeks ago

Last modified 11 days ago

## #14203 new bug

# 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 (5)

### comment:1 Changed 2 weeks ago by

### comment:2 Changed 2 weeks 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 2 weeks 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 11 days ago by

The type of `SMkSigma`

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

from the visible arguments.

### comment:5 Changed 11 days 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.

**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: