Opened 3 months ago

Closed 3 weeks ago

Last modified 3 weeks ago

#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 RyanGlScott

Here's a slightly simpler example that doesn't use singletons. This compiles:

{-# 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 (z :: Apply (p :: a ~> *) (x :: a))

data Bar where
  MkBar :: Foo z -> Bar

And if you ask GHCi for the type of MkBar, you get:

λ> :type +v MkBar
MkBar
  :: forall a (p :: TyFun a * -> *) (x :: a) (z :: Apply p x).
     Foo z -> Bar

But if you try using that:

{-# 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 (z :: Apply (p :: a ~> *) (x :: a))

data Bar where
  MkBar :: forall a (p :: TyFun a * -> *) (x :: a) (z :: Apply p x).
           Foo z -> Bar

It fails:

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:19:16: error:
    • Expected kind ‘Apply p0 x0’, but ‘z’ has kind ‘Apply p x’
    • In the first argument of ‘Foo’, namely ‘z’
      In the type ‘Foo z’
      In the definition of data constructor ‘MkBar’
   |
19 |            Foo z -> Bar
   |                ^

comment:2 Changed 3 months ago by goldfire

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 RyanGlScott

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 goldfire

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 RyanGlScott

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 RyanGlScott

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 Changed 3 weeks ago by simonpj

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 in reply to:  7 Changed 3 weeks ago by RyanGlScott

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 Changed 3 weeks ago by simonpj

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 in reply to:  9 Changed 3 weeks ago by RyanGlScott

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 goldfire

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 RyanGlScott

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 goldfire

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 RyanGlScott

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 simonpj

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 RyanGlScott

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 simonpj

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 RyanGlScott

Resolution: invalid
Status: newclosed

comment:19 Changed 3 weeks ago by goldfire

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.