Opened 8 months ago

Closed 6 months ago

#15079 closed bug (fixed)

GHC HEAD regression: cannot instantiate higher-rank kind

Reported by: RyanGlScott Owned by:
Priority: high Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.5
Keywords: TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4803
Wiki Page:

Description

The following program typechecks on GHC 8.2.2 and 8.4.2:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind
import Data.Void

infixl 4 :==
-- | Heterogeneous Leibnizian equality.
newtype (a :: j) :== (b :: k)
  = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b }

newtype Coerce a = Coerce { uncoerce :: Starify a }
type family Starify (a :: k) :: Type where
  Starify (a :: Type) = a
  Starify _           = Void

coerce :: a :== b -> a -> b
coerce f = uncoerce . hsubst f . Coerce

But GHC HEAD rejects it:

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

Bug.hs:21:34: error:
    • Kind mismatch: cannot unify (c0 :: forall i. i -> *) with:
        Coerce :: forall k. k -> *
      Their kinds differ.
      Expected type: a -> c0 * a
        Actual type: Starify a -> Coerce a
    • In the second argument of ‘(.)’, namely ‘Coerce’
      In the second argument of ‘(.)’, namely ‘hsubst f . Coerce’
      In the expression: uncoerce . hsubst f . Coerce
   |
21 | coerce f = uncoerce . hsubst f . Coerce
   |                                  ^^^^^^

Change History (10)

comment:1 Changed 8 months ago by RyanGlScott

Cc: goldfire added

This regression was introduced in commit e3dbb44f53b2f9403d20d84e27f187062755a089 (Fix #12919 by making the flattener homegeneous.).

comment:2 Changed 8 months ago by RyanGlScott

A more complicated example that also typechecks in 8.2.2 and 8.4.2, but not in GHC HEAD:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

module Bug where

import           Data.Kind
import qualified Data.Type.Equality as Eq
import           GHC.Exts (Any)

infixl 4 :==
-- | Heterogeneous Leibnizian equality.
newtype (a :: j) :== (b :: k)
  = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b }

newtype Flay :: (forall (i :: Type). i -> i -> Type)
             -> forall (j :: Type). j -> forall (k :: Type). k -> Type where
  Flay :: forall (p :: forall (i :: Type). i -> i -> Type)
                 (j :: Type) (k :: Type) (a :: j) (b :: k).
          { unflay :: p a (MassageKind j b) } -> Flay p a b

type family MassageKind (j :: Type) (a :: k) :: j where
  MassageKind j (a :: j) = a
  MassageKind _ _        = Any

fromLeibniz :: forall a b. a :== b -> a Eq.:~: b
fromLeibniz f = unflay $ hsubst f $ Flay Eq.Refl
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:29:42: error:
    • Kind mismatch: cannot unify (p0 :: forall i. i -> i -> *) with:
        (Eq.:~:) :: forall k. k -> k -> *
      Their kinds differ.
      Expected type: p0 k a (MassageKind k a)
        Actual type: a Eq.:~: a
    • In the first argument of ‘Flay’, namely ‘Eq.Refl’
      In the second argument of ‘($)’, namely ‘Flay Eq.Refl’
      In the second argument of ‘($)’, namely ‘hsubst f $ Flay Eq.Refl’
   |
29 | fromLeibniz f = unflay $ hsubst f $ Flay Eq.Refl
   |                                          ^^^^^^^

comment:3 Changed 8 months ago by simonpj

The error message is perplexing, because it suggests that we have failed to prove

forall i. i -> *  ~#  forall k. k -> *

Why? It seems that their visibility-flag differs, as you see if you use -fprint-explicit-foralls (which Joe User will never think of):

T15079.hs:19:34: error:
    * Kind mismatch: cannot unify (c0 :: forall i. i -> *) with:
        Coerce :: forall {k}. k -> *
      Their kinds differ.
      Expected type: a -> c0 * a
        Actual type: Starify a -> Coerce a

tcEqType took no account of the visibility flag before.

Is this anything to do with making the flattener homogeneous?? I see that TcType.tcEqType has grown two new bells

  • It returns a Maybe Bool with this rubric
    -- Nothing    : the types are equal
    -- Just True  : the types differ, and the point of difference is visible
    -- Just False : the types differ, and the point of difference is invisible
    
    But why? We didn't do that before.
  • The treatment of ForAllTy has changed:
        go vis env (ForAllTy (TvBndr tv1 vis1) ty1)
                   (ForAllTy (TvBndr tv2 vis2) ty2)
          = go (isVisibleArgFlag vis1) env (tyVarKind tv1) (tyVarKind tv2)
              <!> go vis (rnBndr2 env tv1 tv2) ty1 ty2
              <!> check vis (vis1 == vis2)
    
    Notice that check vis (vis1 == vis2). That means we say not-equal if the visibility flags differ. But why? These flags are constants, so if they differ now they'll always differ and cannot be unified.

I have no idea what is going on here. Richard can you shed some light?

I'll grant that it's a bit suspicious to say that two forall type are the same if their visibility flags differ. But in this case, yes, Coerce's kind has an Inferred forall, whereas c's kind is Specified. Does that mean they are incompatible? I can't foresee all the consequences of such a decision.

At very least, here's a pretty-printer suggestion: if we do print a forall at all (as we do in this error message) maybe we should always display its visibility status? Otherwise error messages like this are desperately confusing.

comment:4 Changed 8 months ago by RyanGlScott

I too find it rather bizarre that the visibilities of each type variable binder have to line up when instantiating a higher-rank kind, since that isn't a requirement for higher-rank types:

{-# LANGUAGE RankNTypes #-}

id' x = x

f :: (forall a. a -> a) -> b -> c -> (b, c)
f g b c = (g b, g c)

h :: b -> c -> (b, c)
h = f id'

h typechecks, despite the fact that the type of id' is forall {p}. p -> p (i.e., with an inferred variable), and f is supposed to take an argument of type forall a. a -> a (i.e., with a specified variable).

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

comment:5 Changed 8 months ago by RyanGlScott

Now that I have a better understanding of why this is failing, here's a simpler program which demonstrates the issue (this typechecks on GHC 8.4.2, but not HEAD):

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

newtype Foo (f :: forall (a :: Type). a -> Type) = MkFoo (f Int)
data InferredProxy a = MkInferredProxy

foo :: Foo InferredProxy
foo = MkFoo MkInferredProxy
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:11:13: error:
    • Kind mismatch: cannot unify (f0 :: forall a. a -> *) with:
        InferredProxy :: forall k. k -> *
      Their kinds differ.
      Expected type: f0 * Int
        Actual type: InferredProxy Int
    • In the first argument of ‘MkFoo’, namely ‘MkInferredProxy’
      In the expression: MkFoo MkInferredProxy
      In an equation for ‘foo’: foo = MkFoo MkInferredProxy
   |
11 | foo = MkFoo MkInferredProxy
   |             ^^^^^^^^^^^^^^^

comment:6 Changed 8 months ago by simonpj

We await the Sage of Bryn-Mawr.

comment:7 Changed 6 months ago by RyanGlScott

Richard and I discussed this yesterday. We noted that:

  1. The interaction between higher-rank kinds and binder visibility has many parallels with other unexpected properties of higher-rank kinds. In particular, because there are (currently) no type-level lambdas, higher-rank kinds' foralls are more rigid than their type-level counterparts. As one example, in #13399 it was noted that higher-rank kinds' foralls don't "float" like the ones in higher-rank types. In this sense, it's perhaps somewhat understandable that higher-rank kinds' visibility might also be more rigid.
  2. If we wanted to have a more permissive treatment of invisible binders in higher-rank kinds, then we'd need to come up with a better story. Richard considered various ideas like having a subtyping relation between visibilities, but in the end, he concluded that anything we could think of was likely far too complicated for such little payoff.

Thus, the conclusion we reached was that we should keep the current behavior, and make note of this behavior in the users' guide.

comment:8 Changed 6 months ago by RyanGlScott

Differential Rev(s): Phab:D4803
Status: newpatch

comment:9 Changed 6 months ago by Ben Gamari <ben@…>

In bc9a838/ghc:

Document #15079 in the users' guide

Trac #15079 revealed an interesting limitation in the interaction
between variable visibility and higher-rank kinds. We (Richard and I)
came to the conclusion that this is an acceptable (albeit surprising)
limitation, so this documents in the users' guide to hopefully eliminate
some confusion for others in the future.

Test Plan: Read it

Reviewers: goldfire, bgamari

Reviewed By: bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15079

Differential Revision: https://phabricator.haskell.org/D4803

comment:10 Changed 6 months ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.