GitLab

The following program typechecks on GHC 8.6.1-alpha1:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module SGenerics where

import Data.Kind
import Data.Type.Equality
import Data.Void

-----
-- singletons machinery
-----

data family Sing :: forall k. k -> Type

data instance Sing :: () -> Type where
  STuple0 :: Sing '()

type Refuted a = a -> Void
data Decision a = Proved a | Disproved (Refuted a)

-----
-- A stripped down version of GHC.Generics
-----

data U1 = MkU1
data instance Sing (z :: U1) where
  SMkU1 :: Sing MkU1

-----

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)
  sTof  :: forall (a :: k).     Sing a -> PTo (PFrom a) :~: a
  sFot  :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a

-----

instance Generic () where
  type Rep () = U1
  from () = MkU1
  to MkU1 = ()

instance PGeneric () where
  type PFrom '()   = MkU1
  type PTo   'MkU1 = '()

instance SGeneric () where
  sFrom STuple0 = SMkU1
  sTo   SMkU1   = STuple0
  sTof  STuple0 = Refl
  sFot  SMkU1   = Refl

-----

class SDecide k where
  -- | Compute a proof or disproof of equality, given two singletons.
  (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
  default (%~) :: forall (a :: k) (b :: k). (SGeneric 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) ->
      let r :: PTo (PFrom a) :~: PTo (PFrom b)
          r = Refl

          sTof1 :: PTo (PFrom a) :~: a
          sTof1 = sTof s1

          sTof2 :: PTo (PFrom b) :~: b
          sTof2 = sTof s2
      in Proved (sym sTof1 `trans` r `trans` sTof2)
    Disproved contra -> Disproved (\Refl -> contra Refl)

instance SDecide U1 where
  SMkU1 %~ SMkU1 = Proved Refl

instance SDecide ()

However, it throws a Core Lint error with -dcore-lint. The full error is absolutely massive, so I'll attach it separately. Here is the top-level bit:

*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
    In the expression: <elided>
    From-type of Cast differs from type of enclosed expression
    From-type: U1
    Type of enclosed expr: Rep ()
    Actual enclosed expr: PFrom a_a1Fm
    Coercion used in cast: Sym (D:R:Rep()[0])

Trac metadata

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