[GHC] #15577: TypeApplications-related infinite loop (GHC 8.6+ only)

[GHC]

#15577: TypeApplications-related infinite loop (GHC 8.6+ only)
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.5
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  TypeApplications, TypeInType       |
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  performance bug
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following program will loop infinitely when compiled on GHC 8.6 or
 HEAD:

 {{{#!hs
 {-# 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
    |     ^^^^
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15577>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler