Opened 11 months ago

Last modified 8 months ago

#15869 new bug

Discrepancy between seemingly equivalent type synonym and type family

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.6.2
Keywords: TypeFamilies, TypeInType, VisibleDependentQuantification 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 (last modified by RyanGlScott)

Consider the following code:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}

{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

type KindOf1 (a :: k) = k
type family KindOf2 (a :: k) :: Type where
  KindOf2 (a :: k) = k

data A (a :: Type) :: a -> Type
type family Apply1 (f :: KindOf1 A) (a :: Type) (x :: a) :: Type where
  Apply1 f a x = f a x

Apply1 kind-checks, which is just peachy. Note that Apply1 uses KindOf1, which is a type synonym. Suppose I wanted to swap out KindOf1 for KindOf2, which is (seemingly) an equivalent type family. I can define this:

type family Apply2 (f :: KindOf2 A) -- (f :: forall a -> a -> Type)
                   (a :: Type)
                   (x :: a)
                :: Type where
  Apply2 f a x = f a x

However, GHC rejects this!

$ /opt/ghc/8.6.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:25:10: error:
    • Expecting two more arguments to ‘f’
      Expected kind ‘KindOf2 A’, but ‘f’ has kind ‘* -> a -> *’
    • In the first argument of ‘Apply2’, namely ‘f’
      In the type family declaration for ‘Apply2’
   |
25 |   Apply2 f a x = f a x
   |          ^

I find this quite surprising, since I would have expected KindOf1 and KindOf2 to be functionally equivalent. Even providing explicit foralls does not make it kind-check:

type family Apply2 (f :: KindOf2 A) -- (f :: forall a -> a -> Type)
                   (a :: Type)
                   (x :: a)
                :: Type where
  forall (f :: KindOf2 A) (a :: Type) (x :: a).
    Apply2 f a x = f a x

Although the error message does change a bit:

$ ~/Software/ghc3/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:26:20: error:
    • Expected kind ‘* -> a -> *’, but ‘f’ has kind ‘KindOf2 A’
    • In the type ‘f a x’
      In the type family declaration for ‘Apply2’
   |
26 |     Apply2 f a x = f a x
   |                    ^^^^^

Change History (11)

comment:1 Changed 11 months ago by RyanGlScott

This isn't the only discrepancy I've encountered (although this is the most prominent example that I've uncovered). Another, slightly more minor discrepancy can be found in this program:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall -fprint-explicit-foralls #-}
module Bug where

import Data.Kind

type KindOf1 (a :: k) = k
type family KindOf2 (a :: k) :: Type where
  KindOf2 (a :: k) = k

data A (a :: Type) :: a -> Type

f :: KindOf1 A
f = undefined

g = f
h = g

Compiling this yields the following warnings:

$ /opt/ghc/8.6.2/bin/ghci Bug.hs
GHCi, version 8.6.2: 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:1: warning: [-Wmissing-signatures]
    Top-level binding with no type signature: g :: forall {a}. a -> *
   |
19 | g = f
   | ^

Bug.hs:20:1: warning: [-Wmissing-signatures]
    Top-level binding with no type signature: h :: forall {a}. a -> *
   |
20 | h = g
   | ^

Note the inferred type signatures for g and h (Side note: it's a bit weird that their inferred types are forall {a}. a -> * and not, say, forall a -> a -> *. But that's not the main issue here.)

Now, if you redefine f to use KindOf2 in its type signature:

f :: KindOf2 A
f = undefined

Recompiling the module will instead yield these warnings:

$ /opt/ghc/8.6.2/bin/ghci Bug.hs
GHCi, version 8.6.2: 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:1: warning: [-Wmissing-signatures]
    Top-level binding with no type signature: g :: forall a -> a -> *
   |
19 | g = f
   | ^

Bug.hs:20:1: warning: [-Wmissing-signatures]
    Top-level binding with no type signature: h :: forall {a}. a -> *
   |
20 | h = g
   | ^

Notice that the inferred type of g is now forall a -> a -> *, whereas before it was forall {a}. a -> *! Quite strange. (And to make things stranger, the inferred type of h is different from that of g.)

Last edited 9 months ago by RyanGlScott (previous) (diff)

comment:2 Changed 11 months ago by goldfire

Lots of bugs here!

  1. I would expect Apply1 to be rejected without an explicit forall in the equation, giving the polytype of f.
  1. The error message for Apply2 shouldn't say that it expects for arguments to f. The rest of the error message is perhaps confusing, but it's not unreasonable.
  1. The version of Apply2 with the explicit forall in the equation should be accepted.
  1. In the g and h with KindOf1: Their types should be forall a -> a -> Type, not what GHC is reporting.
  1. Ditto for h in the KindOf2 case.

Note that the inferred nature (as opposed to specified) of a is a non-bug: when you don't write a type signature, you don't get specified variables. But of course these should be required, not invisible or specified.

Version 0, edited 11 months ago by goldfire (next)

comment:3 Changed 11 months ago by RyanGlScott

Keywords: TypeInType added

comment:4 Changed 9 months ago by RyanGlScott

Description: modified (diff)

comment:5 Changed 9 months ago by RyanGlScott

While implementing visible dependent quantification (VDQ), I decided to revisit commment:2. Here are some of my findings:

  • I think (4) and (5) are ultimately non-issues, at least for the time being. This is because you won't be able to define f (or g or h) in the first place:
Bug.hs:17:6: error:
    • Illegal visible, dependent quantification in the type of a term:
      forall a -> a -> *
      (GHC does not yet support this)
    • In the expansion of type synonym ‘KindOf1’
      In the type signature: f :: KindOf1 A
   |
17 | f :: KindOf1 A
   |      ^^^^^^^^^

Since terms aren't meant to have types with VDQ in them, I don't think it's worth fretting over (4) and (5). Of course, if VDQ does ever become permitted in terms, perhaps this will pop back up.

  • (1) appears to be unrelated to VDQ and is actually a quirk of ImpredicativeTypes. Here is an example to illustrate what I mean:
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Kind

type family F (f :: forall a. a -> Type) where
  F f = f Int

This doesn't typecheck:

Bug.hs:9:5: error:
    • Expected kind ‘forall a. a -> *’, but ‘f’ has kind ‘* -> k0’
    • In the first argument of ‘F’, namely ‘f’
      In the type family declaration for ‘F’
  |
9 |   F f = f Int
  |     ^

However, if you enable ImpredicativeTypes, then it does typecheck! It's unclear to me why exactly that is, however.

comment:6 Changed 9 months ago by simonpj

If you don't have impredicative-types, then surely the example in the second bullet of comment:5 should be rejected!

But still, the error message looks deeply strange.

comment:7 Changed 9 months ago by RyanGlScott

To be clear, I am in agreement with you that the program in the second bullet point of comment:5 should be rejected if ImpredicativeTypes is not enabled. I am simply wondering if it being accepted with ImpredicativeTypes enabled should count as a bug in its own right. (It's such a squirrelly extension that I can never tell whether it's working as intended or not.)

comment:8 Changed 9 months ago by RyanGlScott

(2) might also be its own issue, since you can trigger the "expecting more arguments" error without VDQ:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

type family F

type family G (f :: F) where
  G f = f Int
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:8:5: error:
    • Expecting one more argument to ‘f’
      Expected kind ‘F’, but ‘f’ has kind ‘* -> k0’
    • In the first argument of ‘G’, namely ‘f’
      In the type family declaration for ‘G’
  |
8 |   G f = f Int
  |     ^

comment:9 Changed 9 months ago by RyanGlScott

I wonder if (3) has anything to do with #9269? KindOf2 A is a bit weird in that it's an application of a type family that returns forall a -> a -> Type, which is a polymorphic type. Normally, GHC disallows that—you wouldn't be able to define type family FAA where FAA = forall a -> a -> Type, for instance. Yet KindOf2 offers a way around this restriction, so perhaps (3) is a manifestation of GHC trying to deal with something it doesn't know how to reason about.

Then again, KindOf2 A seems to work in other places, as comment:1 demonstrates. It's just in type family equations where things go haywire.

comment:10 Changed 9 months ago by RyanGlScott

It's entirely possible that (2) is actually a duplicate of #14319, especially in light of comment:8. (Then again, it's not clear why KindOf2 A isn't reducing in that type family equation in the first place—see comment:9.)

comment:11 Changed 8 months ago by RyanGlScott

Keywords: VisibleDependentQuantification added
Note: See TracTickets for help on using tickets.