[GHC] #11948: GHC forgets constraints
#11948: GHC forgets constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Possibly related: #10338 The following program should compile, but fails with the error: {{{ Could not deduce (Bar (F zq) zq) arising from a use of ‘bar’ from the context (Bar (Foo (F zq)) (Foo zq)) bound by the type signature for bug :: Bar (Foo (F zq)) (Foo zq) => Foo (F zq) -> Foo zq }}} This is definitely incorrect: I am providing a `Bar` constraint in the context of `bug`, but GHC is asking for constraints so that it can resolve to the instance declared in Bar.hs. A few workarounds I've found so far, which may or may not help find the bug: 1. Adding `-XTypeFamilies` to Main.hs makes the program compile. 2. ''Removing'' the type signature from `x` in `bug` makes the program compile. 3. Defining `bug` without a `let` as `bug sk = bar sk :: Foo zq` or `bug sk = bar sk` makes the program compile. Main.hs: {{{ {-# LANGUAGE FlexibleContexts, ScopedTypeVariables #-} import Bar bug :: forall zq . (Bar (Foo (F zq)) (Foo zq)) => Foo (F zq) -> Foo zq bug sk = let x = bar sk :: Foo zq in x }}} Bar.hs {{{ {-# LANGUAGE MultiParamTypeClasses, TypeFamilies #-} module Bar where type family F b newtype Foo r = Foo r type instance F (Foo r) = Foo (F r) class Bar a b where bar :: a -> b instance (Bar a b) => Bar (Foo a) (Foo b) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11948> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11948: GHC forgets constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.2 Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: => 8.0.2 @@ -24,1 +24,1 @@ - Main.hs: + **Main.hs:** @@ -26,1 +26,1 @@ - {{{ + {{{#!hs @@ -28,0 +28,2 @@ + + module Main where @@ -39,1 +41,1 @@ - Bar.hs + **Bar.hs** @@ -41,1 +43,1 @@ - {{{ + {{{#!hs New description: Possibly related: #10338 The following program should compile, but fails with the error: {{{ Could not deduce (Bar (F zq) zq) arising from a use of ‘bar’ from the context (Bar (Foo (F zq)) (Foo zq)) bound by the type signature for bug :: Bar (Foo (F zq)) (Foo zq) => Foo (F zq) -> Foo zq }}} This is definitely incorrect: I am providing a `Bar` constraint in the context of `bug`, but GHC is asking for constraints so that it can resolve to the instance declared in Bar.hs. A few workarounds I've found so far, which may or may not help find the bug: 1. Adding `-XTypeFamilies` to Main.hs makes the program compile. 2. ''Removing'' the type signature from `x` in `bug` makes the program compile. 3. Defining `bug` without a `let` as `bug sk = bar sk :: Foo zq` or `bug sk = bar sk` makes the program compile. **Main.hs:** {{{#!hs {-# LANGUAGE FlexibleContexts, ScopedTypeVariables #-} module Main where import Bar bug :: forall zq . (Bar (Foo (F zq)) (Foo zq)) => Foo (F zq) -> Foo zq bug sk = let x = bar sk :: Foo zq in x }}} **Bar.hs** {{{#!hs {-# LANGUAGE MultiParamTypeClasses, TypeFamilies #-} module Bar where type family F b newtype Foo r = Foo r type instance F (Foo r) = Foo (F r) class Bar a b where bar :: a -> b instance (Bar a b) => Bar (Foo a) (Foo b) }}} -- Comment: This is reproducible with 8.0.1-rc3. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11948#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11948: GHC forgets constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.2 Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): This is a very delicate example. You have, roughly {{{ class C a where op :: Int -> a instance C a => C [a] where ... f :: forall z. C [z] => blah f = ...(op 3 :: [z]).... }}} So arising from the call to `op` we need to solve `C [z]`. There are two ways to solve this: * From the `instance` declaration * From the `C [z] => ...` in the type signature for `f` If we choose the former, type checking will fail. But generally speaking it is ''good'' to reduce class constraints using instance declarations. It's very odd to have a type signature that ''overlaps'' the instance. GHC makes some effort to get this "right", by prioritising solving against "givens", but it's a bit of a hopeless task. After all, it might look like {{{ f = ...(h (op 3)).... }}} where after a great deal of constraint solving, functional dependencies, type function reduction, etc etc, we finally discover that `h`'s argument must have type `[z]`. In this particular case, GHC is trying to infer the most general type for `x`: {{{ let x = bar sk :: Foo zq }}} Arising from `bar` we get the constraint `Bar (Foo (F sk)) (Foo sk)`. When inferring the most general type for `bar` we simplify the constraint as much as possible, using the class `instance` declaration. If you use `MonoLocalBinds` GHC does not attempt to generalise the type of `bar`. So now the (still delicate) prioritisation scheme works, and the program compiles. This why adding `TypeFamilies` helps: `TypeFamilies` implies `MonoLocalBinds`. Anyway the robust solution is to use the `instance` declaration to simplify the constraint for `bar`: {{{ bug :: forall zq . (Bar (F zq) zq) => Foo (F zq) -> Foo zq }}} Maybe GHC should warn about type signatures that have constraints that are reducible with class `instance`s, since they are so fragile. That would be a very worthwhile improvement. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11948#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11948: GHC forgets constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.2 Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"9421b0c77122d40bf72665ea9f90dca64a0a0ae2/ghc" 9421b0c/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="9421b0c77122d40bf72665ea9f90dca64a0a0ae2" Warn about simplifiable class constraints Provoked by Trac #11948, this patch adds a new warning to GHC -Wsimplifiable-class-constraints It warns if you write a class constraint in a type signature that can be simplified by an existing instance declaration. Almost always this means you should simplify it right now; type inference is very fragile without it, as #11948 shows. I've put the warning as on-by-default, but I suppose that if there are howls of protest we can move it out (as happened for -Wredundant- constraints. It actually found an example of an over-complicated context in CmmNode. Quite a few tests use these weird contexts to trigger something else, so I had to suppress the warning in those. The 'haskeline' library has a few occurrences of the warning (which I think should be fixed), so I switched it off for that library in warnings.mk. The warning itself is done in TcValidity.check_class_pred. HOWEVER, when type inference fails we get a type error; and the error suppresses the (informative) warning. So as things stand, the warning only happens when it doesn't cause a problem. Not sure what to do about this, but this patch takes us forward, I think. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11948#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11948: GHC forgets constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.0.2 Component: Compiler | Version: 7.10.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_fail/T11948 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => typecheck/should_fail/T11948 * status: new => closed * resolution: => fixed Comment: OK I've added a warning for simplifiable class constraints. I anticipate a discussion about whether it should be on by default, but currently it is. Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11948#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11948: GHC forgets constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.0.2 Component: Compiler | Version: 7.10.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_fail/T11948 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by crockeea): Thanks for your work on this Simon. The warning is better than the current state of things. I do want to point out that while there are good reasons for simplifying constraints from instance declarations, it can also be a good thing **not** to. In particular, simplifying constraints to help GHC can result in code that has the LHS of the instance in many places, all of which have to be updated when the instance changes. Second, these simplified contexts might not make sense. For example: if I have an `instance (F a) => Foo (G a)` and a function `bar :: Foo (G a) => ...` where `bar` calls some function of `Foo` on type `G a`, GHC will now suggest (if I understand correctly) `bar :: (F a) => ...`. However, `bar` might not use any functions from `F` at all, and it may not involve the type `a` directly. Someone not intimately familiar with the code could be confused by this odd set of constraints. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11948#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11948: GHC forgets constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.0.2 Component: Compiler | Version: 7.10.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_fail/T11948 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes, I guess that's a good point. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11948#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11948: GHC forgets constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 7.10.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_fail/T11948 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thomie): * milestone: 8.0.2 => 8.2.1 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11948#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11948: GHC forgets constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 7.10.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_fail/T11948 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"643706e44935cd15c2248e5345dadd3e9804688e/ghc" 643706e4/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="643706e44935cd15c2248e5345dadd3e9804688e" Narrow the warning for simplifiable constraints In Trac #11948 I added the warning -Wsimplifiable-class-constraints which warns if the class constraints in a type signature are simplifiable. But in fact the fragility it warns about only happens with NoMonoLocalBinds, so this patch switches off the warning if you have MonoLocalBinds (and suggests using it in the error message). See Note [Simplifiable given constraints] in TcValidity. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11948#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC