Opened 11 months ago

Closed 11 months ago

Last modified 11 months ago

#14450 closed bug (fixed)

GHCi spins forever

Reported by: Iceland_jack Owned by:
Priority: high Milestone: 8.4.1
Component: Compiler Version: 8.2.1
Keywords: TypeInType, PolyKinds Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time performance bug Test Case: polykinds/T14450
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The following code compiles just fine (8.3.20170920)

{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #-}

import Data.Kind

data TyFun :: Type -> Type -> Type

type a ~> b = TyFun a b -> Type

type Cat ob = ob -> ob -> Type

type SameKind (a :: k) (b :: k) = (() :: Constraint)

type family 
  Apply (f :: a ~> b) (x :: a) :: b where
  Apply IddSym0 x = Idd x

class Varpi (f :: i ~> j) where
  type Dom (f :: i ~> j) :: Cat i
  type Cod (f :: i ~> j) :: Cat j

  varpa :: Dom f a a' -> Cod f (Apply f a) (Apply f a')

type family 
  Idd (a::k) :: k where
  Idd (a::k) = a

data IddSym0 :: k ~> k where
  IddSym0KindInference :: IddSym0 l

instance Varpi (IddSym0 :: Type ~> Type) where
  type Dom (IddSym0 :: Type ~> Type) = (->)
  type Cod (IddSym0 :: Type ~> Type) = (->)

  varpa :: (a -> a') -> (a -> a')
  varpa = id

But if you change the final instance to

instance Varpi (IddSym0 :: k ~> k) where
  type Dom (IddSym0 :: Type ~> Type) = (->)

it sends GHC for a spin.

Change History (10)

comment:1 Changed 11 months ago by RyanGlScott

Milestone: 8.4.1
Priority: normalhigh
Type of failure: None/UnknownCompile-time performance bug

This is a regression from GHC 8.0.2, which simply gives an error message:

$ /opt/ghc/8.0.2/bin/ghci Bug3.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug3.hs, interpreted )

Bug3.hs:31:12: error:
    • Expected kind ‘k ~> k’, but ‘IddSym0’ has kind ‘Type ~> Type’
    • In the first argument of ‘Dom’, namely
        ‘(IddSym0 :: Type ~> Type)’
      In the type instance declaration for ‘Dom’
      In the instance declaration for ‘Varpi (IddSym0 :: k ~> k)’

This bug first appeared in commit b207b536ded40156f9adb168565ca78e1eef2c74 (Generalize kind of the (->) tycon).

comment:2 Changed 11 months ago by bgamari

Alright, I can have a look. Sadly -ddump-tc-trace doesn't give any hints.

comment:3 Changed 11 months ago by bgamari

Alright, with master -ddump-tc-trace is a bit more useful. While looping it appears to dump

Start solver pipeline {
  work item = [D] _ {1}:: (k_aWv :: *)
                          GHC.Prim.~# (* :: *) (CTyEqCan)
  inerts = {Equalities: [D] _ {1}:: (k_aWv :: *)
                                    GHC.Prim.~# (TYPE q_a20F[tau:1] :: *) (CTyEqCan)
                        [W] hole{a20K} {1}:: (k_aWv :: *) GHC.Prim.~# (* :: *) (CTyEqCan)
                        [W] hole{a20M} {1}:: (k_aWv :: *)
                                             GHC.Prim.~# (TYPE q_a20F[tau:1] :: *) (CTyEqCan)
            Unsolved goals = 2}
  rest of worklist = WL {Eqs = [WD] hole{a20I} {0}:: (TYPE
                                                        r_a20G[tau:1] :: *)
                                                     GHC.Prim.~# (k_aWv :: *) (CNonCanonical)}
runStage canonicalization {
  workitem   =  [D] _ {1}:: (k_aWv :: *)
                            GHC.Prim.~# (* :: *) (CTyEqCan)
can_eq_nc
  False
  [D] _ {1}:: (k_aWv :: *) GHC.Prim.~# (* :: *)
  nominal equality
  k_aWv
  k_aWv
  *
  *
can_eq_nc
  False
  [D] _ {1}:: (k_aWv :: *) GHC.Prim.~# (* :: *)
  nominal equality
  k_aWv
  k_aWv
  *
  *
flatten { FM_FlattenAll k_aWv
flatten } k_aWv
flatten { FM_FlattenAll *
flatten } *
can_eq_nc
  True
  [D] _ {1}:: (k_aWv :: *) GHC.Prim.~# (* :: *)
  nominal equality
  k_aWv
  k_aWv
  *
  *
end stage canonicalization }
runStage interact with inerts {
  workitem   =  [D] _ {1}:: (k_aWv :: *)
                            GHC.Prim.~# (* :: *) (CTyEqCan)
Can't solve tyvar equality
  LHS: k_aWv :: *
  RHS: * :: *
addInertEq {
  Adding new inert equality: [D] _ {1}:: (k_aWv :: *)
                                         GHC.Prim.~# (* :: *) (CTyEqCan)
Kick out, tv = k_aWv
  n-kicked = 1
  kicked_out = WL {Eqs = [D] _ {1}:: (k_aWv :: *)
                                     GHC.Prim.~# (TYPE q_a20F[tau:1] :: *) (CTyEqCan)}
  Residual inerts = {Equalities: [W] hole{a20K} {1}:: (k_aWv :: *)
                                                      GHC.Prim.~# (* :: *) (CTyEqCan)
                                 [W] hole{a20M} {1}:: (k_aWv :: *)
                                                      GHC.Prim.~# (TYPE
                                                                     q_a20F[tau:1] :: *) (CTyEqCan)
                     Unsolved goals = 2}
addInertEq }
end stage interact with inerts }
Step 3424[l:1,d:1] Kept as inert:
    [D] _ {1}:: (k_aWv :: *) GHC.Prim.~# (* :: *)
End solver pipeline (discharged) }
-----------------------------

In particular, unless I've misunderstood something, this strikes me as quite odd,

Can't solve tyvar equality
  LHS: k_aWv :: *
  RHS: * :: *

There's no sign that k_aWv is a skolem so why is the solver not simply instantiating it at *?

comment:4 Changed 11 months ago by bgamari

Cc: goldfire added

I think I may need to bring Richard in on this one.

comment:5 Changed 11 months ago by goldfire

OK -- I'll take a look in due course.

comment:6 Changed 11 months ago by simonpj

I know what is happening here; fix coming

comment:7 Changed 11 months ago by Simon Peyton Jones <simonpj@…>

In 0a851903/ghc:

Fix a TyVar bug in the flattener

A year ago I gave up on trying to rigorously separate TyVars
from TcTyVars, and instead allowed TyVars to appear rather more
freely in types examined by the constraint solver:

   commit 18d0bdd3848201882bae167e3b15fd797d217e93
   Author: Simon Peyton Jones <simonpj@microsoft.com>
   Date:   Wed Nov 23 16:00:00 2016 +0000

   Allow TyVars in TcTypes

See Note [TcTyVars in the typechecker] in TcType.

However, TcFlatten.flatten_tyvar1 turned out to treat
a TyVar specially, and implicitly assumed that it could
not have an equality constraint in the inert set.  Wrong!

This caused Trac #14450.  Fortunately it is easily fixed,
by deleting code.

comment:8 Changed 11 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: polykinds/T14450

comment:9 Changed 11 months ago by Iceland_jack

Is this an instance of the same bug? Loops on 8.3.20170920 and 8.2

{-# Language KindSignatures, TypeOperators, PolyKinds, DataKinds, TypeInType, TypeFamilies, AllowAmbiguousTypes #-}

import Data.Kind

type a-->b = (a, b) -> Type

type Cat k = k -> k -> Type

class F (f::k-->k') where
  type D f :: Cat k
  type C f :: Cat k'
  f :: D f a a' -> C d (App f a) (App f a')

data DupSym0 :: a --> (a, a)

type family
  App (f::a-->b) (x::a) :: b where
  App DupSym0 a = '(a, a)

instance F DupSym0 where
  type D DupSym0 = (->)

comment:10 Changed 11 months ago by RyanGlScott

That program errors for me on the latest GHC HEAD:

$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.3.20171111: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:21:20: error:
    • Expected kind ‘k -> k -> *’, but ‘(->)’ has kind ‘* -> * -> *’
    • In the type ‘(->)’
      In the type instance declaration for ‘D’
      In the instance declaration for ‘F DupSym0’
   |
21 |   type D DupSym0 = (->)
   |                    ^^^^

So I'd wager that it's the same issue.

Note: See TracTickets for help on using tickets.