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
Cc: | goldfire added |
---|
comment:2 Changed 8 months ago by
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
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 thatcheck 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
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).
comment:5 Changed 8 months ago by
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:7 Changed 6 months ago by
Richard and I discussed this yesterday. We noted that:
- 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. - 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
Differential Rev(s): | → Phab:D4803 |
---|---|
Status: | new → patch |
comment:10 Changed 6 months ago by
Resolution: | → fixed |
---|---|
Status: | patch → closed |
This regression was introduced in commit e3dbb44f53b2f9403d20d84e27f187062755a089 (Fix #12919 by making the flattener homegeneous.).