Opened 7 weeks ago

Closed 4 weeks ago

#15577 closed bug (fixed)

TypeApplications-related infinite loop (GHC 8.6+ only)

Reported by: RyanGlScott Owned by:
Priority: high Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.5
Keywords: TypeApplications, TypeInType Cc: simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time performance bug Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (7)

comment:1 Changed 7 weeks ago by RyanGlScott

Here's a somewhat smaller example:

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

import Data.Kind
import Data.Proxy
import Data.Type.Equality

type family F (x :: f (a :: k)) :: f a

f :: forall k (f :: k -> Type) (a :: k) (r :: f a). Proxy r -> F r :~: r
f = undefined

g :: forall (f :: Type -> Type) (a :: Type) (r :: f a). Proxy r -> F r :~: r
g r | Refl <- f -- Uncommenting the line below makes it work again
                -- @Type
                @f @a @r r
    = Refl

comment:2 Changed 7 weeks ago by RyanGlScott

Cc: simonpj added

This regression was introduced in commit a32c8f7514c8192fa064537fb93d5a5c224991a0 (Use dischargeFunEq consistently).

comment:3 Changed 6 weeks ago by simonpj

I know what is happening here. In TcCanonical.canCFunEqCan we have

canCFunEqCan ev fn tys fsk
  = do { (tys', cos, kind_co) <- flattenArgsNom ev fn tys
                        -- cos :: tys' ~ tys
       ; let lhs_co  = mkTcTyConAppCo Nominal fn cos
                        -- :: F tys' ~ F tys
             new_lhs = mkTyConApp fn tys'

             flav    = ctEvFlavour ev
       ; (ev', fsk')
              -- See Note [canCFunEqCan]
           <- if isTcReflCo kind_co
              then
                ..normal, homo-kinded case..
              else
                ..hetero-kinded case..
...

The note is a good explanation; read it.

In the example above, we get a Given CFunEqCan that is homo-kinded. But kind_co turns out not to be ReflCo but rather some giant (but still reflexive) coercion. So we fall ito the heter-kinded case.

Then, as the Note says, we make a new homo-kinded CFunEqCan. But when we end up processing that (as we do), we think it too is hetero-kinded, and so we do it all over again. Forever.

For now I have fixed it by using isTcReflexiveCo instead of isTcReflCo. But isn't it suspicious that flattenArgsNom returns a complicated giant coercion? And that gets right back into flatten_args_fast and flatten_args_slow, which we were discussing last week. I'll leave that for Richard and Ningning to ponder.

Meanwhile I think I have fixed the loop. Validating now....

Here for completeness is part of the log

canCFunEqCan: non-refl
  Kind co: (Sym (GRefl nominal (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                                        {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                                         {co_a28p})
                                                              ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                                                        {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                                                         {co_a28p})
                                                                              ->_N <*>_N))
                     (Sym ((Sym (GRefl nominal f_a28k[sk:1]
                                     {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p})
                           ->_N <*>_N))) ; (Sym (GRefl nominal a_a28l[sk:1]
                                                     (({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                                              {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                                               {co_a28p})
                                                                    ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                                                              {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                                                               {co_a28p})
                                                                                    ->_N <*>_N))) ; GRefl nominal a_a28l[sk:1]
                                                                                                        (({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                                                                                                 {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                                                                                                  {co_a28p})
                                                                                                                       ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                                                                                                                 {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                                                                                                                  {co_a28p})
                                                                                                                                       ->_N <*>_N)))) (Sym (GRefl nominal (r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1]
                                                                                                                                                                                                               {co_a28p})
                                                                                                                                                                (Sym (Sym (GRefl nominal f_a28k[sk:1]
                                                                                                                                                                               {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                                                                                                                                                {co_a28p}))) ; (Sym (GRefl nominal r_a28m[sk:1]
                                                                                                                                                                                                                         (Sym {co_a28w} ; GRefl nominal f_a28k[sk:1]
                                                                                                                                                                                                                                              {co_a28p})) ; GRefl nominal r_a28m[sk:1]
                                                                                                                                                                                                                                                                (Sym {co_a28w} ; GRefl nominal f_a28k[sk:1]
                                                                                                                                                                                                                                                                                     {co_a28p})))
  RHS: fsk_a29k[fsk:2] :: (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                                   {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                                    {co_a28p})
                                                         ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                                                   {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                                                    {co_a28p})
                                                                         ->_N <*>_N))
                            (r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1]
                                                                 {co_a28p})
  LHS: F (f_a28k[sk:1] |> {co_a28p})
         (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                  {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p})
                                        ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                                  {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                                   {co_a28p})
                                                        ->_N <*>_N))
         (r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1]
                                              {co_a28p})
         r_a28x[tau:1]
         :: (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                     {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                      {co_a28p})
                                           ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                                     {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                                      {co_a28p})
                                                           ->_N <*>_N))
              (r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1]
                                                   {co_a28p})
  New LHS F (f_a28k[sk:1] |> {co_a28p})
            (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                     {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                      {co_a28p})
                                           ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                                     {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                                      {co_a28p})
                                                           ->_N <*>_N))
            (r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1]
                                                 {co_a28p})
            r_a28x[tau:1]
            :: (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                        {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                         {co_a28p})
                                              ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1]
                                                                        {co_a28p}) ; GRefl nominal f_a28k[sk:1]
                                                                                         {co_a28p})
                                                              ->_N <*>_N))
                 (r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1]
                                                      {co_a28p})

This shows stuff right at the start of the hetero-kinded 'else' branch above

  • kind_co is the giant coercion returned by flattenArgsNom
  • RHS is the fsk, and I show its kind, which is (a |> ..) (r |> ..)
  • LHS is the original function application, (F tys) in the code above; again I show its kind, which is identical to that of fks.
  • New LHS is the new function application after flattening, (F tys') in the code. You'll note that it is identical to (F tys)!

All this work for nothing. Surely flattenArgsNom can be a bit cleverer?

comment:4 Changed 6 weeks ago by Simon Peyton Jones <simonpj@…>

In 2e226a46/ghc:

canCFunEqCan: use isTcReflexiveCo (not isTcReflCo)

As Trac #15577 showed, it was possible for a /homo-kinded/
constraint to trigger the /hetero-kinded/ branch of canCFunEqCan,
and that triggered an infinite loop.

The fix is easier, but there remains a deeper questions: why is
the flattener producing giant refexive coercions?

comment:5 Changed 6 weeks ago by simonpj

OK, I've committed a fix -- worth merging.

BUT please leave the ticket open.

Richard, Ningning: could you possibly look at whether there's a simple change to flatten_args that would eliminate these giant coercions in the case where there is literally no flattening to be done?.

Last edited 6 weeks ago by simonpj (previous) (diff)

comment:6 Changed 6 weeks ago by RyanGlScott

Status: newmerge

Marking this as merge so that Ben will see it. (But, as simonpj notes in comment:5, don't actually close this ticket until Richard/Ningning has reviewed it.)

comment:7 Changed 4 weeks ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.