#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 13 months ago by
Milestone: | → 8.4.1 |
---|---|
Priority: | normal → high |
Type of failure: | None/Unknown → Compile-time performance bug |
comment:2 Changed 13 months ago by
Alright, I can have a look. Sadly -ddump-tc-trace
doesn't give any hints.
comment:3 Changed 13 months ago by
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 13 months ago by
Cc: | goldfire added |
---|
I think I may need to bring Richard in on this one.
comment:8 Changed 13 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → polykinds/T14450 |
comment:9 Changed 13 months ago by
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 13 months ago by
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.
This is a regression from GHC 8.0.2, which simply gives an error message:
This bug first appeared in commit b207b536ded40156f9adb168565ca78e1eef2c74 (
Generalize kind of the (->) tycon
).