GitLab

The following program will loop infinitely when compiled on GHC 8.6 or HEAD:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind
import Data.Type.Equality

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

class Generic1 (f :: k -> Type) where
  type Rep1 f :: k -> Type

class PGeneric1 (f :: k -> Type) where
  type From1 (z :: f a)      :: Rep1 f a
  type To1   (z :: Rep1 f a) :: f a

class SGeneric1 (f :: k -> Type) where
  sFrom1 :: forall (a :: k) (z :: f a).      Sing z -> Sing (From1 z)
  sTo1   :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)

class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k -> Type) where
  sTof1 :: forall (a :: k) (z :: f a).      Sing z -> To1 (From1 z)        :~: z
  sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> From1 (To1 r :: f a) :~: r

foo :: forall (f :: Type -> Type) (a :: Type) (r :: Rep1 f a).
       VGeneric1 f
    => Sing r -> From1 (To1 r :: f a) :~: r
foo x
  | Refl <- sFot1 -- Uncommenting the line below makes it work again:
                  -- @Type
                  @f @a @r x
  = Refl

This is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:35:20: error:
    • Expecting one more argument to ‘f’
      Expected a type, but ‘f’ has kind ‘* -> *’
    • In the type ‘f’
      In a stmt of a pattern guard for
                     an equation for ‘foo’:
        Refl <- sFot1 @f @a @r x
      In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
   |
35 |                   @f @a @r x
   |                    ^

Bug.hs:35:23: error:
    • Expected kind ‘f1 -> *’, but ‘a’ has kind ‘*’
    • In the type ‘a’
      In a stmt of a pattern guard for
                     an equation for ‘foo’:
        Refl <- sFot1 @f @a @r x
      In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
    • Relevant bindings include
        x :: Sing r1 (bound at Bug.hs:32:5)
        foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
   |
35 |                   @f @a @r x
   |                       ^

Bug.hs:35:26: error:
    • Couldn't match kind ‘* -> *’ with ‘*’
      When matching kinds
        f1 :: * -> *
        Rep1 f1 a1 :: *
      Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’
    • In the type ‘r’
      In a stmt of a pattern guard for
                     an equation for ‘foo’:
        Refl <- sFot1 @f @a @r x
      In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
    • Relevant bindings include
        x :: Sing r1 (bound at Bug.hs:32:5)
        foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
   |
35 |                   @f @a @r x
   |                          ^

Bug.hs:35:28: error:
    • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’
      When matching kinds
        a1 :: *
        'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep
    • In the fourth argument of ‘sFot1’, namely ‘x’
      In a stmt of a pattern guard for
                     an equation for ‘foo’:
        Refl <- sFot1 @f @a @r x
      In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
    • Relevant bindings include
        x :: Sing r1 (bound at Bug.hs:32:5)
        foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
   |
35 |                   @f @a @r x
   |                            ^

Bug.hs:36:5: error:
    • Could not deduce: From1 (To1 r1) ~ r1
      from the context: r0 ~ From1 (To1 r0)
        bound by a pattern with constructor:
                   Refl :: forall k (a :: k). a :~: a,
                 in a pattern binding in
                      pattern guard for
                      an equation for ‘foo’
        at Bug.hs:33:5-8
      ‘r1’ is a rigid type variable bound by
        the type signature for:
          foo :: forall (f1 :: * -> *) a1 (r1 :: Rep1 f1 a1).
                 VGeneric1 f1 =>
                 Sing r1 -> From1 (To1 r1) :~: r1
        at Bug.hs:(29,1)-(31,43)
      Expected type: From1 (To1 r1) :~: r1
        Actual type: r1 :~: r1
    • In the expression: Refl
      In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
    • Relevant bindings include
        x :: Sing r1 (bound at Bug.hs:32:5)
        foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
   |
36 |   = Refl
   |     ^^^^

Trac metadata

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