[GHC] #13320: Unfortunate compiler loop when creating type loop (with UndecidableInstances)

#13320: Unfortunate compiler loop when creating type loop (with UndecidableInstances) -------------------------------------+------------------------------------- Reporter: Ptival | Owner: (none) Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple UndecidableInstances loop | Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I'm afraid this will simply be seen as "that's what happens when you use UndecidableInstances", but I might as well document this issue I had. Trying to play with a "Trees that Grow" syntax, I encountered an issue when making a mistake, that can be boiled down to the following: {{{#!hs {-# language ConstraintKinds, FlexibleContexts, TypeFamilies, UndecidableInstances #-} module Loop where import GHC.Exts (Constraint) import Test.QuickCheck type family X_Var ξ data TermX ξ = Var (X_Var ξ) type ForallX (φ :: * -> Constraint) ξ = ( φ (X_Var ξ) ) --genTerm :: ForallX Arbitrary ξ => Int -> Gen (TermX ξ) genTerm 0 = Var <$> arbitrary genTerm n = Var <$> genTerm (n - 1) --instance ForallX Arbitrary ξ => Arbitrary (TermX ξ) where --arbitrary = sized genTerm }}} This code will compile correctly, and generate: {{{#!hs genTerm :: (X_Var ξ ~ TermX ξ, Arbitrary (TermX ξ), Eq t, Num t) => t -> Gen (TermX ξ) }}} Which is correct (though, not the type I had intended, since my code had a mistake). Now, if you uncomment the "instance" line only, the compiler will loop. Adding the commented out type, of course, gives a type error where it's due. I was just wondering whether this type of error failed with the loops that should be caught by the compiler. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13320 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13320: Unfortunate compiler loop when creating type loop (with UndecidableInstances) -------------------------------------+------------------------------------- Reporter: Ptival | Owner: (none) Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | UndecidableInstances loop Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Here's a version with no dependencies: {{{#!hs {-# language ConstraintKinds, FlexibleContexts, TypeFamilies, UndecidableInstances #-} module Loop where import GHC.Exts (Constraint) data QCGen newtype Gen a = MkGen { unGen :: QCGen -> Int -> a } sized :: (Int -> Gen a) -> Gen a sized f = MkGen (\r n -> let MkGen m = f n in m r n) class Arbitrary a where arbitrary :: Gen a type family X_Var ξ data TermX ξ = Var (X_Var ξ) type ForallX (φ :: * -> Constraint) ξ = ( φ (X_Var ξ) ) -- Uncommenting the line below gives a proper type error. --genTerm :: ForallX Arbitrary ξ => Int -> Gen (TermX ξ) genTerm 0 = Var <$> arbitrary genTerm n = Var <$> genTerm (n - 1) instance ForallX Arbitrary ξ => Arbitrary (TermX ξ) where arbitrary = sized genTerm }}} At the very least, compiling this on GHC HEAD doesn't loop forever, but instead fails with a stack overflow: {{{ Bug.hs:25:1: error: Reduction stack overflow; size = 201 When simplifying the following type: Arbitrary (TermX ξ0) Use -freduction-depth=0 to disable this check (any upper bound you could choose might fail unpredictably with minor updates to GHC, so disabling the check is recommended if you're sure that type checking should terminate) | 25 | genTerm 0 = Var <$> arbitrary | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13320#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13320: Unfortunate compiler loop when creating type loop (with UndecidableInstances) -------------------------------------+------------------------------------- Reporter: Ptival | Owner: (none) Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | UndecidableInstances loop Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Ptival: Old description:
I'm afraid this will simply be seen as "that's what happens when you use UndecidableInstances", but I might as well document this issue I had.
Trying to play with a "Trees that Grow" syntax, I encountered an issue when making a mistake, that can be boiled down to the following:
{{{#!hs {-# language ConstraintKinds, FlexibleContexts, TypeFamilies, UndecidableInstances #-}
module Loop where
import GHC.Exts (Constraint) import Test.QuickCheck
type family X_Var ξ
data TermX ξ = Var (X_Var ξ)
type ForallX (φ :: * -> Constraint) ξ = ( φ (X_Var ξ) )
--genTerm :: ForallX Arbitrary ξ => Int -> Gen (TermX ξ) genTerm 0 = Var <$> arbitrary genTerm n = Var <$> genTerm (n - 1)
--instance ForallX Arbitrary ξ => Arbitrary (TermX ξ) where --arbitrary = sized genTerm
}}}
This code will compile correctly, and generate:
{{{#!hs genTerm :: (X_Var ξ ~ TermX ξ, Arbitrary (TermX ξ), Eq t, Num t) => t -> Gen (TermX ξ) }}}
Which is correct (though, not the type I had intended, since my code had a mistake).
Now, if you uncomment the "instance" line only, the compiler will loop.
Adding the commented out type, of course, gives a type error where it's due.
I was just wondering whether this type of error failed with the loops that should be caught by the compiler.
New description: I'm afraid this will simply be seen as "that's what happens when you use UndecidableInstances", but I might as well document this issue I had. Trying to play with a "Trees that Grow" syntax, I encountered an issue when making a mistake, that can be boiled down to the following: {{{#!hs {-# language ConstraintKinds, FlexibleContexts, TypeFamilies, UndecidableInstances #-} module Loop where import GHC.Exts (Constraint) import Test.QuickCheck type family X_Var ξ data TermX ξ = Var (X_Var ξ) type ForallX (φ :: * -> Constraint) ξ = ( φ (X_Var ξ) ) --genTerm :: ForallX Arbitrary ξ => Int -> Gen (TermX ξ) genTerm 0 = Var <$> arbitrary genTerm n = Var <$> genTerm (n - 1) --instance ForallX Arbitrary ξ => Arbitrary (TermX ξ) where --arbitrary = sized genTerm }}} This code will compile correctly, and generate: {{{#!hs genTerm :: (X_Var ξ ~ TermX ξ, Arbitrary (TermX ξ), Eq t, Num t) => t -> Gen (TermX ξ) }}} Which is correct (though, not the type I had intended, since my code had a mistake). Now, if you uncomment the "instance" line only, the compiler will loop. Adding the commented out type, of course, gives a type error where it's due. I was just wondering whether this type of error fell within the "loops that should be caught by the compiler". -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13320#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13320: Unfortunate compiler loop when creating type loop (with UndecidableInstances) -------------------------------------+------------------------------------- Reporter: Ptival | Owner: dfeuer Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | UndecidableInstances loop Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * owner: (none) => dfeuer Comment: This appears to be fixed now. I will add the test case. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13320#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13320: Unfortunate compiler loop when creating type loop (with UndecidableInstances) -------------------------------------+------------------------------------- Reporter: Ptival | Owner: dfeuer Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | UndecidableInstances loop Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Ah, commit 859dc65369e8a9722514046246dd32b683c8b4a9 (Yet another attempt at inferring the right quantification) was what fixed this. Hooray! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13320#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13320: Unfortunate compiler loop when creating type loop (with UndecidableInstances) -------------------------------------+------------------------------------- Reporter: Ptival | Owner: dfeuer Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | UndecidableInstances loop Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Great! Please add the test case though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13320#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13320: Unfortunate compiler loop when creating type loop (with
UndecidableInstances)
-------------------------------------+-------------------------------------
Reporter: Ptival | Owner: dfeuer
Type: bug | Status: new
Priority: low | Milestone:
Component: Compiler | Version: 8.0.1
Resolution: | Keywords:
| UndecidableInstances loop
Operating System: Unknown/Multiple | Architecture:
Type of failure: Compile-time | Unknown/Multiple
crash or panic | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by David Feuer

#13320: Unfortunate compiler loop when creating type loop (with UndecidableInstances) -------------------------------------+------------------------------------- Reporter: Ptival | Owner: dfeuer Type: bug | Status: closed Priority: low | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: fixed | UndecidableInstances loop Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): phab:D3532 Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * status: new => closed * component: Compiler => Compiler (Type checker) * differential: => phab:D3532 * resolution: => fixed * milestone: => 8.2.1 Comment: Test case added as phab:D3532. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13320#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13320: Unfortunate compiler loop when creating type loop (with UndecidableInstances) -------------------------------------+------------------------------------- Reporter: Ptival | Owner: dfeuer Type: bug | Status: closed Priority: low | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: fixed | UndecidableInstances loop Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): phab:D3532 Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): Test merged with 561553fe424e2f2e3500b635655fe6d9c294c666. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13320#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC