GitLab

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)
   |                                                    ^^^^

Trac metadata

Trac field	Value
Version	8.4.1-alpha1
Type	Bug
TypeOfFailure	OtherFailure
Priority	high
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture