Opened 5 months ago
Closed 3 months ago
#14720 closed bug (fixed)
GHC 8.4.1-alpha regression with TypeInType
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | high | Milestone: | 8.4.1 |
Component: | Compiler (Type checker) | Version: | 8.4.1-alpha1 |
Keywords: | TypeInType | Cc: | goldfire |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | dependent/should_compile/T14720 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
GHC 8.2.2 is able to typecheck this code:
{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module SGenerics where import Data.Kind (Type) import Data.Type.Equality ((:~:)(..), sym, trans) import Data.Void data family Sing (z :: k) class Generic (a :: Type) where type Rep a :: Type from :: a -> Rep a to :: Rep a -> a class PGeneric (a :: Type) where type PFrom (x :: a) :: Rep a type PTo (x :: Rep a) :: a class SGeneric k where sFrom :: forall (a :: k). Sing a -> Sing (PFrom a) sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k) class (PGeneric k, SGeneric k) => VGeneric k where sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a sFot :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a data Decision a = Proved a | Disproved (a -> Void) class SDecide k where (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b) default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k)) => Sing a -> Sing b -> Decision (a :~: b) s1 %~ s2 = case sFrom s1 %~ sFrom s2 of Proved (Refl :: PFrom a :~: PFrom b) -> case (sTof s1, sTof s2) of (Refl, Refl) -> Proved Refl Disproved contra -> Disproved (\Refl -> contra Refl)
But GHC 8.4.1-alpha2 cannot:
$ /opt/ghc/8.4.1/bin/ghc Bug.hs [1 of 1] Compiling SGenerics ( Bug.hs, Bug.o ) Bug.hs:44:52: error: • Could not deduce: PFrom a ~ PFrom a from the context: b ~ a bound by a pattern with constructor: Refl :: forall k (a :: k). a :~: a, in a lambda abstraction at Bug.hs:44:37-40 Expected type: PFrom a :~: PFrom b Actual type: PFrom a :~: PFrom a NB: ‘PFrom’ is a non-injective type family • In the first argument of ‘contra’, namely ‘Refl’ In the expression: contra Refl In the first argument of ‘Disproved’, namely ‘(\ Refl -> contra Refl)’ • Relevant bindings include contra :: (PFrom a :~: PFrom b) -> Void (bound at Bug.hs:44:15) s2 :: Sing b (bound at Bug.hs:40:9) s1 :: Sing a (bound at Bug.hs:40:3) (%~) :: Sing a -> Sing b -> Decision (a :~: b) (bound at Bug.hs:40:3) | 44 | Disproved contra -> Disproved (\Refl -> contra Refl) | ^^^^
Change History (5)
comment:1 Changed 5 months ago by
Cc: | goldfire added |
---|
comment:2 Changed 5 months ago by
I'm pretty sure this is #12919. It works on my branch, held up due to performance problems. It's being actively worked on by @alexvieth, to whom I've gratefully delegated fixing those performance problems. But when I say active, I mean it: Alex sent me some results offline this morning.
comment:3 Changed 5 months ago by
For the record, here's a smaller test case:
{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module SGenerics where import Data.Kind (Type) type family R :: Type data family Sing (z :: R) type family PFrom (x :: Type) :: R u :: forall (a :: R). Sing a u = u v :: forall (a :: Type). Sing (PFrom a) v = u
comment:5 Changed 3 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → dependent/should_compile/T14720 |
Note: See
TracTickets for help on using
tickets.
This regression was introduced in commit 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 (
Improve error messages around kind mismatches.
).I'm unsure if this is related to #14038 (which was also triggered by the same commit).