[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
#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
participants (1)
-
GHC