[GHC] #10338: GHC Forgets Constraints
#10338: GHC Forgets Constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- This is possibly fixed by #10195, but I don't have a convenient means of testing it. At any rate, this testcase is considerably simpler than the one in #10195. {{{#!hs {-# LANGUAGE TypeFamilies, FlexibleContexts, GADTs, MultiParamTypeClasses #-} type family F r class (Functor t) => T t r where fromScalar :: r -> t r data Foo t r where Foo :: t (F r) -> Foo t r Scalar :: r -> Foo t r toF :: r -> F r toF = undefined convert :: (T t (F r)) => Foo t r -> Foo t r convert (Scalar c) = let fromScalar' = fromScalar in Foo $ fromScalar' $ toF c }}} This code compiles with GHC 7.8.4. When I add a generic instance for `T` (which requires `FlexibleInstances`): `instance (Functor t, Num r) => T t r` GHC complains: {{{#!hs Could not deduce (Num (F r)) arising from a use of ‘fromScalar’ from the context (T t (F r)) bound by the type signature for convert :: (T t (F r)) => Foo t r -> Foo t r at Main.hs:(17,12)-(18,23) In the expression: fromScalar In an equation for ‘fromScalar'’: fromScalar' = fromScalar In the expression: let fromScalar' = fromScalar in Foo $ fromScalar' $ toF c }}} Of course the problem can be fixed by adding a type signature to `fromScalar` and adding `ScopedTypeVariables`: {{{#!hs convert :: forall t r . (T t (F r)) => Foo t r -> Foo t r convert (Scalar c) = let fromScalar' = fromScalar :: F r -> t (F r) in Foo $ fromScalar' $ toF c }}} Like #10195, this is triggered when a generic instance is in scope. The (main) problem of course is that GHC tries to match the generic instance instead of using the `T (F r)` constraint supplied by `convert`. A secondary issue is that I think the example should have the same behavior pre- and post-instance, i.e either both should compile or both should not compile. I'm not sure if a monomorphism restriction is actually being triggered here or if that's just a red herring. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10338 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10338: GHC Forgets Constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Yes this is confusing. No it's not #10195. Here's what happens. When GHC comes across the local binding `let fromScalar' = fromScalar`, it tries to find its most general type. To do so it instantiates the call to `fromScalar` with fresh unification variables `t0` and `r0`, and generates the constraint `T t0 r0`. Now it tries to simplify that constraint, and succeeds with the top level instance declaration; and that is where things go wrong; we get the inferred type {{{ fromScalar' :: forall t r. (Functor t, Num r) => r -> t r }}} Why doesn't it refrain from simplifying `T t0 r0` because of the in-scope constraint `T t (F r)`? Answer: the most general type of a local binding is computed by calling the constraint simplifer during constraint generation. It's a break with the general plan to first do constraint generation and only then simplify constraints. If we didn't attempt to generalise the binding for `fromScalar'` we would not do this early call to the constraint solver, and all would be well (at this point the "given overlap" fix in #10195 would kick in). You might think that `MonoLocalBinds` would make this happen, but actually `MonoLocalBinds` attempts to generalise even local bindings that have no non-top-level type variables, such as this one. And indeed usually generalising is a good thing. Maybe there should be a way to turn off local generalisation altogether. Congratulations on dicovering this. I had previously thought that `MonoLocalBinds` would make the constraint solver completely well behaved, but this example shows that I wasn't quite right. I don't see an easy fix, and it seems very much a corner case so probably doesn't justify the work (and code complexity) for a non-easy fix. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10338#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10338: GHC Forgets Constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by rwbarton): The fact that the binding of `fromScalar'` is a local one is not actually important here: the program with {{{ instance (Functor t, Num r) => T t r fromScalar' a = fromScalar a -- or turn on NoMonomorphismRestriction convert :: (T t (F r)) => Foo t r -> Foo t r convert (Scalar c) = Foo $ fromScalar' $ toF c }}} also gives the error about "Could not deduce (Num (F r)) arising from a use of ‘fromScalar'’". -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10338#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10338: GHC Forgets Constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): But that's very reasonable isn't it? What type do you expect to be inferred for `fromScalar'`? Well, you get a constraint `T t r` arising from the call to `fromScalar` in its RHS, and GHC solves that constraint using the instance declaration, so we get the inferred type {{{ fromScalar' :: (Functor t, Num r) => r -> t r }}} And now you can see why you get the complaint when it's called in `convert`. What did you think would happen? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10338#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10338: GHC Forgets Constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by crockeea): I've got a new test case for what I assume is this bug. Unfortunately, I can't find a workaround in this case. {{{#!hs {-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables, ConstraintKinds, KindSignatures, TypeFamilies, FlexibleInstances #-} import GHC.Prim import Control.Monad class Unsat (a :: * -> *) c class Qux (t :: * -> *) where type QCtx t q :: Constraint qux :: (QCtx t q, Monad rnd) => v -> rnd (t q) instance Qux t where type QCtx t q = (Unsat t q) class (Qux c) => C (c :: * -> *) r mymap :: c Double -> c i mymap = undefined foo :: forall c z v rnd . (C c z, Monad rnd, Num z) => v -> rnd (c z) foo svar = liftM mymap $ qux svar I've tried a wide array of explicit type sigs on `foo`, but nothing seems to make it find the dictionary for `Qux` inherited from `C`. I really need a fix for this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10338#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10338: GHC Forgets Constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Well all the GHCs I have say {{{ T10338a.hs:27:26: Could not deduce (Unsat c Double) arising from a use of `qux' from the context (C c z, Monad rnd, Num z) bound by the type signature for foo :: (C c z, Monad rnd, Num z) => v -> rnd (c z) at T10338a.hs:26:8-69 }}} And that is totally correct. Every call to `qux` gives rise to a constraint `QCtx t q`. Nothing provides that constraint, certainly not `C c z`. But in fact the instance for `Qux t` says that `QCtx t q` simplifies to `Unsat t q`. And we are stuck. (The call to `qux` also gives rise to a `Qux c` constraint, and that is indeed satisfied from the `C c z` superclass.) I'm at a loss for why you think this program should typecheck. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10338#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10338: GHC Forgets Constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by crockeea): Ah, I see. I saw "could not deduce Unsat" and thought it was the same bug. My mistake. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10338#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10338: GHC Forgets Constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: 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 dfeuer): If you're not using overlapping instances, then you can solve the problem by imposing {{{#!hs class (Functor t, Num r) => T t r where }}} In that context, the only (hypothetical) downside is that you don't have the option of hiding the constraint. I don't know if that's a real concern. If you are using overlapping instances, ~~you've dug yourself into a hole and I don't have much sympathy for you~~ the `ScopedTypeVariables` work- around doesn't seem too onerous. It would be interesting to see if this can be reproduced using code that makes sense ''without'' `OverlappingInstances`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10338#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10338: GHC Forgets Constraints -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: 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 crockeea: @@ -61,1 +61,1 @@ - instead of using the `T (F r)` constraint supplied by `convert`. + instead of using the `T t (F r)` constraint supplied by `convert`. New description: This is possibly fixed by #10195, but I don't have a convenient means of testing it. At any rate, this testcase is considerably simpler than the one in #10195. {{{#!hs {-# LANGUAGE TypeFamilies, FlexibleContexts, GADTs, MultiParamTypeClasses #-} type family F r class (Functor t) => T t r where fromScalar :: r -> t r data Foo t r where Foo :: t (F r) -> Foo t r Scalar :: r -> Foo t r toF :: r -> F r toF = undefined convert :: (T t (F r)) => Foo t r -> Foo t r convert (Scalar c) = let fromScalar' = fromScalar in Foo $ fromScalar' $ toF c }}} This code compiles with GHC 7.8.4. When I add a generic instance for `T` (which requires `FlexibleInstances`): `instance (Functor t, Num r) => T t r` GHC complains: {{{#!hs Could not deduce (Num (F r)) arising from a use of ‘fromScalar’ from the context (T t (F r)) bound by the type signature for convert :: (T t (F r)) => Foo t r -> Foo t r at Main.hs:(17,12)-(18,23) In the expression: fromScalar In an equation for ‘fromScalar'’: fromScalar' = fromScalar In the expression: let fromScalar' = fromScalar in Foo $ fromScalar' $ toF c }}} Of course the problem can be fixed by adding a type signature to `fromScalar` and adding `ScopedTypeVariables`: {{{#!hs convert :: forall t r . (T t (F r)) => Foo t r -> Foo t r convert (Scalar c) = let fromScalar' = fromScalar :: F r -> t (F r) in Foo $ fromScalar' $ toF c }}} Like #10195, this is triggered when a generic instance is in scope. The (main) problem of course is that GHC tries to match the generic instance instead of using the `T t (F r)` constraint supplied by `convert`. A secondary issue is that I think the example should have the same behavior pre- and post-instance, i.e either both should compile or both should not compile. I'm not sure if a monomorphism restriction is actually being triggered here or if that's just a red herring. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10338#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC