[GHC] #14846: Renamer hangs (because of -XInstanceSigs?)
#14846: Renamer hangs (because of -XInstanceSigs?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: InstanceSigs | Operating System: Unknown/Multiple TypeInType | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# Language RankNTypes, TypeInType, EmptyCase, GADTs, FlexibleInstances, ConstraintKinds, UndecidableInstances, AllowAmbiguousTypes, InstanceSigs #-} import Data.Kind import Data.Proxy type Cat ob = ob -> ob -> Type data Struct :: (k -> Constraint) -> Type where S :: Proxy (a::k) -> Struct (cls::k -> Constraint) type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls) data AStruct :: Struct cls -> Type where AStruct :: cls a => AStruct (Structured a cls) class StructI (structured::Struct (cls :: k -> Constraint)) where struct :: AStruct structured instance (Structured xx cls ~ structured, cls xx) => StructI structured where struct :: AStruct (Structured xx cls) struct = AStruct data Hom :: Cat k -> Cat (Struct cls) where class Category (cat::Cat ob) where i :: StructI a => ríki a a instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where i :: forall a. StructI a => Hom ríki a a i = case struct :: AStruct (Structured a cls) of }}} Running on 8.2.1 and 8.5.20180105 both loop until interrupted {{{ $ ghci -ignore-dot-ghci 199.hs GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 199.hs, interpreted ) ^CInterrupted.
}}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14846 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14846: Renamer hangs (because of -XInstanceSigs?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: InstanceSigs | TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I can't reproduce this with either version of GHC you give: {{{ $ /opt/ghc/8.2.2/bin/ghci Bug.hs GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:29:8: error: • Couldn't match type ‘ríki1’ with ‘Hom ríki’ ‘ríki1’ is a rigid type variable bound by the type signature for: i :: forall k2 (cls1 :: k2 -> Constraint) (a :: Struct cls1) (ríki1 :: Struct cls1 -> Struct cls1 -> *). StructI a => ríki1 a a at Bug.hs:29:8-42 Expected type: ríki1 a a Actual type: Hom ríki a a • When checking that instance signature for ‘i’ is more general than its signature in the class Instance sig: forall (a :: Struct cls0). StructI a => Hom ríki a a Class sig: forall k (cls :: k -> Constraint) (a :: Struct cls) (ríki :: Struct cls -> Struct cls -> *). StructI a => ríki a a In the instance declaration for ‘Category (Hom ríki)’ | 29 | i :: forall a. StructI a => Hom ríki a a | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Bug.hs:30:12: error: • Could not deduce: cls1 a1 arising from a use of ‘struct’ from the context: Category ríki bound by the instance declaration at Bug.hs:28:10-65 or from: StructI a bound by the type signature for: i :: forall (a :: Struct cls0). StructI a => Hom ríki a a at Bug.hs:29:8-42 • In the expression: struct :: AStruct (Structured a cls) In the expression: case struct :: AStruct (Structured a cls) of In an equation for ‘i’: i = case struct :: AStruct (Structured a cls) of | 30 | i = case struct :: AStruct (Structured a cls) of | ^^^^^^ }}} What am I missing? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14846#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14846: Renamer hangs (because of -XInstanceSigs?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: InstanceSigs | TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Ah, I forgot. You have to add `ScopedTypeVariables`, that should be enough. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14846#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14846: Renamer hangs (because of -XInstanceSigs?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: InstanceSigs | TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Old description:
{{{#!hs {-# Language RankNTypes, TypeInType, EmptyCase, GADTs, FlexibleInstances, ConstraintKinds, UndecidableInstances, AllowAmbiguousTypes, InstanceSigs #-}
import Data.Kind import Data.Proxy
type Cat ob = ob -> ob -> Type
data Struct :: (k -> Constraint) -> Type where S :: Proxy (a::k) -> Struct (cls::k -> Constraint)
type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls)
data AStruct :: Struct cls -> Type where AStruct :: cls a => AStruct (Structured a cls)
class StructI (structured::Struct (cls :: k -> Constraint)) where struct :: AStruct structured
instance (Structured xx cls ~ structured, cls xx) => StructI structured where struct :: AStruct (Structured xx cls) struct = AStruct
data Hom :: Cat k -> Cat (Struct cls) where
class Category (cat::Cat ob) where i :: StructI a => ríki a a
instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where i :: forall a. StructI a => Hom ríki a a i = case struct :: AStruct (Structured a cls) of }}}
Running on 8.2.1 and 8.5.20180105 both loop until interrupted
{{{ $ ghci -ignore-dot-ghci 199.hs GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 199.hs, interpreted ) ^CInterrupted.
}}}
New description: {{{#!hs {-# Language RankNTypes, TypeInType, EmptyCase, GADTs, FlexibleInstances, ConstraintKinds, Undecida bleInstances, AllowAmbiguousTypes, InstanceSigs, ScopedTypeVariables #-} import Data.Kind import Data.Proxy type Cat ob = ob -> ob -> Type data Struct :: (k -> Constraint) -> Type where S :: Proxy (a::k) -> Struct (cls::k -> Constraint) type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls) data AStruct :: Struct cls -> Type where AStruct :: cls a => AStruct (Structured a cls) class StructI (structured::Struct (cls :: k -> Constraint)) where struct :: AStruct structured instance (Structured xx cls ~ structured, cls xx) => StructI structured where struct :: AStruct (Structured xx cls) struct = AStruct data Hom :: Cat k -> Cat (Struct cls) where class Category (cat::Cat ob) where i :: StructI a => ríki a a instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where -- Commenting out this instance signature makes the issue go away i :: forall a. StructI a => Hom ríki a a i = case struct :: AStruct (Structured a cls) of }}} Running on 8.2.1 and 8.5.20180105 both loop until interrupted {{{ $ ghci -ignore-dot-ghci 199.hs GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 199.hs, interpreted ) ^CInterrupted.
}}} -- Comment (by RyanGlScott): Thanks. I've updated the original program to reflect this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14846#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14846: Renamer hangs (because of -XInstanceSigs?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: InstanceSigs | TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by RyanGlScott: Old description:
{{{#!hs {-# Language RankNTypes, TypeInType, EmptyCase, GADTs, FlexibleInstances, ConstraintKinds, Undecida bleInstances, AllowAmbiguousTypes, InstanceSigs, ScopedTypeVariables #-}
import Data.Kind import Data.Proxy
type Cat ob = ob -> ob -> Type
data Struct :: (k -> Constraint) -> Type where S :: Proxy (a::k) -> Struct (cls::k -> Constraint)
type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls)
data AStruct :: Struct cls -> Type where AStruct :: cls a => AStruct (Structured a cls)
class StructI (structured::Struct (cls :: k -> Constraint)) where struct :: AStruct structured
instance (Structured xx cls ~ structured, cls xx) => StructI structured where struct :: AStruct (Structured xx cls) struct = AStruct
data Hom :: Cat k -> Cat (Struct cls) where
class Category (cat::Cat ob) where i :: StructI a => ríki a a
instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where -- Commenting out this instance signature makes the issue go away i :: forall a. StructI a => Hom ríki a a i = case struct :: AStruct (Structured a cls) of }}}
Running on 8.2.1 and 8.5.20180105 both loop until interrupted
{{{ $ ghci -ignore-dot-ghci 199.hs GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 199.hs, interpreted ) ^CInterrupted.
}}}
New description: {{{#!hs {-# Language RankNTypes, TypeInType, EmptyCase, GADTs, FlexibleInstances, ConstraintKinds, UndecidableInstances, AllowAmbiguousTypes, InstanceSigs, ScopedTypeVariables #-} import Data.Kind import Data.Proxy type Cat ob = ob -> ob -> Type data Struct :: (k -> Constraint) -> Type where S :: Proxy (a::k) -> Struct (cls::k -> Constraint) type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls) data AStruct :: Struct cls -> Type where AStruct :: cls a => AStruct (Structured a cls) class StructI (structured::Struct (cls :: k -> Constraint)) where struct :: AStruct structured instance (Structured xx cls ~ structured, cls xx) => StructI structured where struct :: AStruct (Structured xx cls) struct = AStruct data Hom :: Cat k -> Cat (Struct cls) where class Category (cat::Cat ob) where i :: StructI a => ríki a a instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where -- Commenting out this instance signature makes the issue go away i :: forall a. StructI a => Hom ríki a a i = case struct :: AStruct (Structured a cls) of }}} Running on 8.2.1 and 8.5.20180105 both loop until interrupted {{{ $ ghci -ignore-dot-ghci 199.hs GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 199.hs, interpreted ) ^CInterrupted.
}}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14846#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14846: Renamer hangs (because of -XInstanceSigs?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: InstanceSigs | TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Actually, this program //doesn't// hang—it actually produces a stack overflow after a certain amount of time! {{{ $ time ~/Software/ghc2/inplace/bin/ghc-stage2 Bug.hs[1 of 1] Compiling Bug ( Bug.hs, Bug.o ) stack overflow: use +RTS -K<size> to increase it real 0m18.986s user 0m18.472s sys 0m0.540s $ ~/Software/ghc2/inplace/bin/ghc-stage2 --version The Glorious Glasgow Haskell Compilation System, version 8.5.20180221 }}} Here's what this looks like in `-ddump-tc-trace`: {{{ runStage interact with inerts { workitem = [WD] $dStructI_a1MK {0}:: StructI (Structured a_a1LU[sk:4] (cls_a1Li[ssk:2] |> {co_a1M2} ->_N <Constraint>_N)) (CDictCan) addFunDepWork [WD] $dStructI_a1MK {0}:: StructI (Structured a_a1LU[sk:4] (cls_a1Li[ssk:2] |> {co_a1M2} ->_N <Constraint>_N)) arising from a use of ‘struct’ at Bug.hs:32:12-17 False arising from the type signature for: i :: forall (a :: Struct cls). StructI a => Hom ríki_a1Lj[ssk:2] a a at Bug.hs:31:8-42 True arising from a functional dependency between constraints: ‘StructI (Structured a_a1LU[sk:4] (cls_a1Li[ssk:2] |> {co_a1M2} ->_N <Constraint>_N))’ arising from a use of ‘struct’ at Bug.hs:32:12-17 ‘StructI a_a1LU[sk:4]’ arising from the type signature for: i :: forall (a :: Struct cls). StructI a => Hom ríki_a1Lj[ssk:2] a a at Bug.hs:31:8-42 at Bug.hs:32:12-17 False end stage interact with inerts } runStage top-level reactions { workitem = [WD] $dStructI_a1MK {0}:: StructI (Structured a_a1LU[sk:4] (cls_a1Li[ssk:2] |> {co_a1M2} ->_N <Constraint>_N)) (CDictCan) doTopReact [WD] $dStructI_a1MK {0}:: StructI (Structured a_a1LU[sk:4] (cls_a1Li[ssk:2] |> {co_a1M2} ->_N <Constraint>_N)) (CDictCan) *** Exception: stack overflow }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14846#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14846: Renamer hangs (because of -XInstanceSigs?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: InstanceSigs | TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): In case you're worried about that `UndecidableInstances` part, here's a version that doesn't use `UndecidableInstances`: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind import Data.Proxy type Cat ob = ob -> ob -> Type data Struct :: (k -> Constraint) -> Type where S :: Proxy (a::k) -> Struct (cls::k -> Constraint) type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls) data AStruct :: Struct cls -> Type where AStruct :: cls a => AStruct (Structured a cls) class StructI xx (structured::Struct (cls :: k -> Constraint)) where struct :: AStruct structured instance (Structured xx cls ~ structured, cls xx) => StructI xx structured where struct :: AStruct (Structured xx cls) struct = AStruct data Hom :: Cat k -> Cat (Struct cls) where class Category (cat::Cat ob) where i :: StructI xx a => ríki a a instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where i :: forall xx a. StructI xx a => Hom ríki a a i = case struct :: AStruct (Structured a cls) of }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14846#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14846: Renamer hangs (because of -XInstanceSigs?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: InstanceSigs | TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Great bug report. Patch coming -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14846#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14846: Renamer hangs (because of -XInstanceSigs?)
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: goldfire
Type: bug | Status: new
Priority: highest | Milestone: 8.6.1
Component: Compiler | Version: 8.5
Resolution: | Keywords: InstanceSigs
| TypeInType
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
| polykinds/T14846
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Changes (by simonpj):
* owner: (none) => goldfire
* testcase: => polykinds/T14846
* priority: normal => highest
* milestone: => 8.6.1
Comment:
Fixed by
{{{
commit e99fdf775540440c1c58dc5ade3c5984dc49246f
Author: Simon Peyton Jones
---------------------------------------------------------------
e99fdf775540440c1c58dc5ade3c5984dc49246f compiler/types/Unify.hs | 59 ++++++++++++++++++--------------- testsuite/tests/polykinds/T14846.hs | 39 ++++++++++++++++++++++ testsuite/tests/polykinds/T14846.stderr | 43 ++++++++++++++++++++++++ testsuite/tests/polykinds/all.T | 1 + 4 files changed, 116 insertions(+), 26 deletions(-) }}} Richard, can you just check my work? I'll leave the ticket open, but assign to you. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14846#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14846: Renamer hangs (because of -XInstanceSigs?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: goldfire Type: bug | Status: merge Priority: normal | Milestone: 8.4.2 Component: Compiler | Version: 8.5 Resolution: | Keywords: InstanceSigs | TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T14846 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * priority: highest => normal * status: new => merge * milestone: 8.6.1 => 8.4.2 Comment: Patch looks good to me. This is a clear bug and shouldn't be hard to merge. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14846#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14846: Renamer hangs (because of -XInstanceSigs?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: 8.4.2 Component: Compiler | Version: 8.5 Resolution: fixed | Keywords: InstanceSigs | TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T14846 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged to `ghc-8.4`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14846#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC