Visible foralls are no longer injective
The following program compiles on GHC HEAD:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Type.Equality
inject :: forall (f :: forall (k :: Type) -> Type)
(a :: Type) (b :: Type).
f a :~: f b
-> a :~: b
inject Refl = Refl
But on this branch, it fails with this error:
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:11: error:
• Couldn't match type ‘f a’ with ‘f0 a’
Expected type: (f a :~: f b) ~> a :~: b
Actual type: (f0 a :~: f0 b) ~> a :~: b
• In the ambiguity check for ‘inject’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
inject :: forall (f :: forall (k :: Type) -> Type)
(a :: Type)
(b :: Type).
f a :~: f b ~> a :~: b
|
10 | inject :: forall (f :: forall (k :: Type) -> Type)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Weird, it's complaining that f
is ambiguous now. If I enable AllowAmbiguousTypes
, then it still fails:
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:15: error:
• Could not deduce: a ~ b
from the context: f b ~ f a
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in an equation for ‘inject’
at Bug.hs:15:8-11
‘a’ is a rigid type variable bound by
the type signature for:
inject :: forall (f :: forall k -> *) a b. (f a :~: f b) ~> a :~: b
at Bug.hs:(11,1)-(14,17)
‘b’ is a rigid type variable bound by
the type signature for:
inject :: forall (f :: forall k -> *) a b. (f a :~: f b) ~> a :~: b
at Bug.hs:(11,1)-(14,17)
Expected type: a :~: b
Actual type: a :~: a
• In the expression: Refl
In an equation for ‘inject’: inject Refl = Refl
• Relevant bindings include
inject :: (f a :~: f b) ~> a :~: b (bound at Bug.hs:15:1)
|
15 | inject Refl = Refl
| ^^^^
Something seems deeply strange here.