Opened 2 years ago

Closed 2 years ago

#14723 closed bug (fixed)

GHC 8.4.1-alpha loops infinitely when typechecking

Reported by: RyanGlScott Owned by:
Priority: highest Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.4.1-alpha1
Keywords: Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time performance bug Test Case: polykinds/T14723
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by RyanGlScott)

This issue prevents jvm-streaming from compiling with GHC 8.4.1-alpha2. Here is my best attempt at minimizing the issue:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug () where

import Data.Kind (Type)
import Data.Proxy (Proxy(..))
import Data.String (fromString)
import Data.Int (Int64)
import GHC.Stack (HasCallStack)
import GHC.TypeLits (Nat, Symbol)

data JType = Iface Symbol

data J (a :: JType)

  :: IO (J ('Iface "java.util.Iterator"))
newIterator = do
    let tblPtr :: Int64
        tblPtr = undefined
    iterator <-
          (loadJavaWrappers >>
                  (Proxy ::
                     Proxy "{ return  new java.util.Iterator() {\n                @Override\n                public native boolean hasNext();\n\n                @Override\n                public native Object next();\n\n                @Override\n                public void remove() {\n                    throw new UnsupportedOperationException();\n                }\n\n                private native void hsFinalize(long tblPtr);\n\n                @Override\n                public void finalize() {\n                    hsFinalize($tblPtr);\n                }\n             } ; }"))
                 (Proxy :: Proxy "inline__method_0"))
                (Proxy :: Proxy "tblPtr"))
               (Proxy :: Proxy 106))
              (tblPtr, ()))
                (fromString "inline__method_0"))
               [coerce tblPtr])))

class Coercible (a :: Type) where
  type Ty a :: JType

class Coercibles xs (tys :: k) | xs -> tys
instance Coercibles () ()
instance (ty ~ Ty x, Coercible x, Coercibles xs tys) => Coercibles (x, xs) '(ty, tys)

  :: forall
     -- k                -- the kind variable shows up in Core
     (args_tys :: k)     -- JType's of arguments
     tyres               -- JType of result
     (input :: Symbol)   -- input string of the quasiquoter
     (mname :: Symbol)   -- name of the method to generate
     (antiqs :: Symbol)  -- antiquoted variables as a comma-separated list
     (line :: Nat)       -- line number of the quasiquotation
     args_tuple          -- uncoerced argument types
     b.                  -- uncoerced result type
     (tyres ~ Ty b, Coercibles args_tuple args_tys, Coercible b, HasCallStack)
  => Proxy input
  -> Proxy mname
  -> Proxy antiqs
  -> Proxy line
  -> args_tuple
  -> Proxy args_tys
  -> IO b
  -> IO b
qqMarker = undefined

With GHC 8.2.2, this is properly rejected by the typechecker:

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

Bug.hs:27:12: error:
    Variable not in scope: loadJavaWrappers :: IO a0
27 |           (loadJavaWrappers >>
   |            ^^^^^^^^^^^^^^^^

Bug.hs:36:16: error:
    Variable not in scope: callStatic :: t0 -> t1 -> [a2] -> IO a1
36 |             (((callStatic
   |                ^^^^^^^^^^

Bug.hs:40:17: error: Variable not in scope: coerce :: Int64 -> a2
40 |                [coerce tblPtr])))
   |                 ^^^^^^

But in GHC 8.4.1-alpha2, this simply hangs forever.

To make things more interesting, if you pass -ddump-tc-trace when compiling, you'll get a panic:

$ /opt/ghc/8.4.1/bin/ghc Bug.hs -ddump-tc-trace
kcLHsQTyVars: cusk
kcTyClGroup: initial kinds
  [rB8 :-> ATcTyCon JType :: *, rB9 :-> APromotionErr RecDataConPE]
  [rB8 :-> ATcTyCon JType :: *, rB9 :-> APromotionErr RecDataConPE]
kcTyClDecl { JType
env2 []
tcExtendBinderStack []
env2 []
tcExtendBinderStack []
lk1 Symbol
  tclvl 1
  * ~ TYPE t_a1qq[tau:1]
  arising from a type equality * ~ TYPE t_a1qq[tau:1]
  tclvl 1
  'GHC.Types.LiftedRep ~ t_a1qq[tau:1]
  arising from a type equality * ~ TYPE t_a1qq[tau:1]
  tclvl 1
  GHC.Types.RuntimeRep ~ GHC.Types.RuntimeRep
  arising from a kind equality arising from
    t_a1qq[tau:1] ~ 'GHC.Types.LiftedRep
u_tys yields no coercion
  t_a1qq[tau:1] :: GHC.Types.RuntimeRep := 'GHC.Types.LiftedRep
u_tys yields no coercion
u_tys yields no coercion
  TYPE t_a1qq[tau:1]
kcLHsQTyVars: not-cuskghc: panic! (the 'impossible' happened)
  (GHC version for x86_64-unknown-linux):

Change History (9)

comment:1 Changed 2 years ago by RyanGlScott

Description: modified (diff)

comment:2 Changed 2 years ago by RyanGlScott

Wow! This regression was also triggered by commit 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 (Improve error messages around kind mismatches.), putting it in good company with #14038 and #14720.

comment:3 Changed 2 years ago by RyanGlScott

Cc: goldfire added

comment:4 Changed 2 years ago by bgamari

Hmm, perhaps we should consider reverting this commit for 8.4. It would be sad to do so, but it seems like it is causing quite some trouble. Thanks for pinpointing these, Ryan!

comment:5 Changed 2 years ago by simonpj

Here's a diagnosis. We have

  class Coercibles k k1 (xs :: k) (tys :: k1) | xs -> tys

  instance forall k (ty :: JType) x xs (tys :: k).
           (ty ~ Ty x, Coercible x, Coercibles * k xs tys) =>
           Coercibles * (JType, k) (x, xs) '(ty, tys)

and a wanted constraint

  [WD] $dCoercibles_a2K3 :: Coercibles *
                                       (JType, k_a2My[tau:1])
                                       (Int64, ())
  args_tys_a2JU :: (JType, kappa1)

Now, from the fundep xs -> tys we generate

  [D] arg_tys_a2JU ~ (ty::JType, tys::kappa2)

where ty, tys, and kappa2 are all fresh unification variables. They are fresh because they they are not directly fixed by (x,xs) in the instance decl, but only indirectly via the context of the instance decl (so-called "liberal" fundeps). This is legitimate.

But this new derived equality is hetero-kinded, so we "park" it (as a CIrredCan) and emit a derived equality on the kinds

  [D] (JType, kappa1) ~ (JType, kappa2)

We solve this, by kappa1 := kappa2. That kicks out the two inert, unsolved constraints, both of which mention kappa1:

  [WD] $dCoercibles_a2K3 :: Coercibles *
                                       (JType, k_a2My[tau:1])
                                       (Int64, ())
  [D] arg_tys_a2JU ~ (ty::JType, tys::kappa2)

Alas, we choose the former to solve; and that simply repeats the entire process from the beginning.

If instead we chose the derived equality constraint, the kappa1 := kappa2 would make the equality homo-kinded, so we'd solve with args_tys_a2JU := (ty,tys); and now the Coercibles constraint matches the instance and can be solved.

And even if the Coercibles constraint doesn't (yet) match an instance, (maybe there's another parameter to the class that prevents the match) provided we've processed all the equalities coming from the fundeps first, we'll find that, if we generate fundeps again, they are all no-ops.

Bottom line: one fix would be to prioritise equality constraints, even if they are Derived. Currently we priorities Wanted constraints in the work-list over Derived, on the grounds that if we solve all the Wanted constraints we may never need to process those Derived ones at all.

Another (possibly better) approach might be to remember when we have generated fundeps from a class constraint, and refrain from doing so a second time. But that seems hard, because as we rewrite the class constraint we may learn more about some of its arguments, and therefore expose more possible fundeps. So it's hard to say when we "have generated the fundeps" from a class constraint.

comment:6 Changed 2 years ago by Simon Peyton Jones <simonpj@…>

In efba0546/ghc:

Prioritise equalities when solving, incl deriveds

We already prioritise equalities when solving, but
Trac #14723 showed that we were not doing so consistently
enough, and as a result the type checker could go into a loop.

See Note [Prioritise equalities] in TcSMonad.

Fixng this bug changed the solve order enough to demonstrate
a problem with fundeps: Trac #14745.

comment:7 Changed 2 years ago by simonpj

Status: newmerge

This is a bad bug, now fixed. Merge if poss.

comment:8 Changed 2 years ago by simonpj

Test Case: polykinds/T14723

comment:9 Changed 2 years ago by bgamari

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