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 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 2 weeks 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 2 weeks 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 11 days ago by goldfire

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 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.

Note: See TracTickets for help on using tickets.