Re: [GHC] #14723: GHC 8.4.1-alpha loops infinitely when typechecking

25 Jan 2018

      #14723: GHC 8.4.1-alpha loops infinitely when typechecking
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.4.1-alpha1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  performance bug                    |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by RyanGlScott:

Old description:
...
This issue prevents `jvm-streaming` from compiling with GHC 8.4.1-alpha2.
Here is my best attempt at minimizing the issue:
{{{#!hs
{-# 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)
newIterator
  :: IO (J ('Iface "java.util.Iterator"))
newIterator = do
    let tblPtr :: Int64
        tblPtr = undefined
    iterator <-
          (loadJavaWrappers >>
         (((((((qqMarker
                  (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 v
oid 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, ()))
             Proxy)
            (((callStatic
                 (fromString
"io.tweag.inlinejava.Inline__jvmstreaming022inplace_Language_Java_Streaming"))
                (fromString "inline__method_0"))
               [coerce tblPtr])))
    undefined
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)
qqMarker
  :: 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
  JType
  []
  []
  []
  []
  *
  []
  []
  []
  []
kcTyClGroup: initial kinds
  [rB8 :-> ATcTyCon JType :: *, rB9 :-> APromotionErr RecDataConPE]
txExtendKindEnv
  [rB8 :-> ATcTyCon JType :: *, rB9 :-> APromotionErr RecDataConPE]
kcTyClDecl { JType
env2 []
tcExtendBinderStack []
env2 []
tcExtendBinderStack []
lk1 Symbol
tcTyVar2a
  Symbol
  *
u_tys
  tclvl 1
  * ~ TYPE t_a1qq[tau:1]
  arising from a type equality * ~ TYPE t_a1qq[tau:1]
u_tys
  tclvl 1
  'GHC.Types.LiftedRep ~ t_a1qq[tau:1]
  arising from a type equality * ~ TYPE t_a1qq[tau:1]
u_tys
  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
writeMetaTyVar
  t_a1qq[tau:1] :: GHC.Types.RuntimeRep := 'GHC.Types.LiftedRep
u_tys yields no coercion
u_tys yields no coercion
checkExpectedKind
  *
  TYPE t_a1qq[tau:1]
  <*>_N
kcLHsQTyVars: not-cuskghc: panic! (the 'impossible' happened)
  (GHC version 8.4.0.20180118 for x86_64-unknown-linux):
        kcConDecl
}}}
New description:

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

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

 newIterator
   :: IO (J ('Iface "java.util.Iterator"))
 newIterator = do
     let tblPtr :: Int64
         tblPtr = undefined
     iterator <-
           (loadJavaWrappers >>
          (((((((qqMarker
                   (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, ()))
              Proxy)
             (((callStatic
                  (fromString
 "io.tweag.inlinejava.Inline__jvmstreaming022inplace_Language_Java_Streaming"))
                 (fromString "inline__method_0"))
                [coerce tblPtr])))
     undefined

 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)

 qqMarker
   :: 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
   JType
   []
   []
   []
   []
   *
   []
   []
   []
   []
 kcTyClGroup: initial kinds
   [rB8 :-> ATcTyCon JType :: *, rB9 :-> APromotionErr RecDataConPE]
 txExtendKindEnv
   [rB8 :-> ATcTyCon JType :: *, rB9 :-> APromotionErr RecDataConPE]
 kcTyClDecl { JType
 env2 []
 tcExtendBinderStack []
 env2 []
 tcExtendBinderStack []
 lk1 Symbol
 tcTyVar2a
   Symbol
   *
 u_tys
   tclvl 1
   * ~ TYPE t_a1qq[tau:1]
   arising from a type equality * ~ TYPE t_a1qq[tau:1]
 u_tys
   tclvl 1
   'GHC.Types.LiftedRep ~ t_a1qq[tau:1]
   arising from a type equality * ~ TYPE t_a1qq[tau:1]
 u_tys
   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
 writeMetaTyVar
   t_a1qq[tau:1] :: GHC.Types.RuntimeRep := 'GHC.Types.LiftedRep
 u_tys yields no coercion
 u_tys yields no coercion
 checkExpectedKind
   *
   TYPE t_a1qq[tau:1]
   <*>_N
 kcLHsQTyVars: not-cuskghc: panic! (the 'impossible' happened)
   (GHC version 8.4.0.20180118 for x86_64-unknown-linux):
         kcConDecl
 }}}

--

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14723#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler