[GHC] #12832: GHC infers too simplified contexts
#12832: GHC infers too simplified contexts -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Incorrect Unknown/Multiple | error/warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I'm almost sure it was working well in GHC 7.*. Let's consider this simple example: {{{ module Main where import Prelude class Monad m => Foo m class Monad m => Bar m class Monad m => Baz m data IM a data I impossible = error "impossible" class Test m a where test :: a -> m () instance {-# OVERLAPPABLE #-} (Foo m, Bar m, Baz m) => Test m a where test _ = return () instance {-# OVERLAPPABLE #-} Test IM a where test = impossible class Run m a where run :: a -> m () main :: IO () main = return () }}} it compiles and runs fine. What should happen when we add the following def? {{{ instance Run m Int where run = test }}} We SHOULD get an error that there is `No instance for (Test m Int) arising from a use of ‘test’`. Instead we get very strange one `No instance for (Foo m) arising from a use of ‘test’.` If we add it, we get the next one `No instance for (Bar m) arising from a use of ‘test’.` etc ... If we comment out the first overlappable instance, we get proper error about missing `Test m Int` context. In fact if we add context `Test m Int` it works in every case, only the inferred error is just wrong. This is a serious problem and here is why. Imagine that we create an API for end-user and we give him the `test` function. Moreover, we know that expanding the context would not bring any further info unless `m` is known. If we create such "impossible" instances like in the example, user will get a very simple error message about a missing context. Right now user gets a big error stack about missing expanded contexts instead of simple one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12832 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12832: GHC infers too simplified contexts -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by danilo2: @@ -5,0 +5,5 @@ + + {-# LANGUAGE FlexibleInstances #-} + {-# LANGUAGE MultiParamTypeClasses #-} + {-# LANGUAGE EmptyDataDecls #-} + New description: I'm almost sure it was working well in GHC 7.*. Let's consider this simple example: {{{ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE EmptyDataDecls #-} module Main where import Prelude class Monad m => Foo m class Monad m => Bar m class Monad m => Baz m data IM a data I impossible = error "impossible" class Test m a where test :: a -> m () instance {-# OVERLAPPABLE #-} (Foo m, Bar m, Baz m) => Test m a where test _ = return () instance {-# OVERLAPPABLE #-} Test IM a where test = impossible class Run m a where run :: a -> m () main :: IO () main = return () }}} it compiles and runs fine. What should happen when we add the following def? {{{ instance Run m Int where run = test }}} We SHOULD get an error that there is `No instance for (Test m Int) arising from a use of ‘test’`. Instead we get very strange one `No instance for (Foo m) arising from a use of ‘test’.` If we add it, we get the next one `No instance for (Bar m) arising from a use of ‘test’.` etc ... If we comment out the first overlappable instance, we get proper error about missing `Test m Int` context. In fact if we add context `Test m Int` it works in every case, only the inferred error is just wrong. This is a serious problem and here is why. Imagine that we create an API for end-user and we give him the `test` function. Moreover, we know that expanding the context would not bring any further info unless `m` is known. If we create such "impossible" instances like in the example, user will get a very simple error message about a missing context. Right now user gets a big error stack about missing expanded contexts instead of simple one. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12832#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12832: GHC infers too simplified contexts -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by danilo2: @@ -5,1 +5,1 @@ - + {-# LANGUAGE NoMonomorphismRestriction #-} New description: I'm almost sure it was working well in GHC 7.*. Let's consider this simple example: {{{ {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE EmptyDataDecls #-} module Main where import Prelude class Monad m => Foo m class Monad m => Bar m class Monad m => Baz m data IM a data I impossible = error "impossible" class Test m a where test :: a -> m () instance {-# OVERLAPPABLE #-} (Foo m, Bar m, Baz m) => Test m a where test _ = return () instance {-# OVERLAPPABLE #-} Test IM a where test = impossible class Run m a where run :: a -> m () main :: IO () main = return () }}} it compiles and runs fine. What should happen when we add the following def? {{{ instance Run m Int where run = test }}} We SHOULD get an error that there is `No instance for (Test m Int) arising from a use of ‘test’`. Instead we get very strange one `No instance for (Foo m) arising from a use of ‘test’.` If we add it, we get the next one `No instance for (Bar m) arising from a use of ‘test’.` etc ... If we comment out the first overlappable instance, we get proper error about missing `Test m Int` context. In fact if we add context `Test m Int` it works in every case, only the inferred error is just wrong. This is a serious problem and here is why. Imagine that we create an API for end-user and we give him the `test` function. Moreover, we know that expanding the context would not bring any further info unless `m` is known. If we create such "impossible" instances like in the example, user will get a very simple error message about a missing context. Right now user gets a big error stack about missing expanded contexts instead of simple one. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12832#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12832: GHC infers too simplified contexts -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): There is a reason for this behaviour. I won't say that it is a ''good'' reason, but it's not an accident. See this note in `TcInstDcls`: {{{ Note [Subtle interaction of recursion and overlap] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this class C a where { op1,op2 :: a -> a } instance {-# OVERLAPPING #-} C [Int] where ... instance {-# OVERLAPPABLE #-} C a => C [a] where op1 x = op2 x ++ op2 x op2 x = ... ... When type-checking the C [a] instance, we need a C [a] dictionary (for the call of op2). If we look up in the instance environment, we find an overlap. And in *general* the right thing is to complain (see Note [Overlapping instances] in InstEnv). But in *this* case it's wrong to complain, because we just want to delegate to the op2 of this same instance. Why is this justified? Because we generate a (C [a]) constraint in a context in which 'a' cannot be instantiated to anything that matches other overlapping instances, or else we would not be executing this version of op1 in the first place. It might even be a bit disguised: nullFail :: C [a] => [a] -> [a] nullFail x = op2 x ++ op2 x instance C a => C [a] where op1 x = nullFail x Precisely this is used in package 'regex-base', module Context.hs. See the overlapping instances for RegexContext, and the fact that they call 'nullFail' just like the example above. The DoCon package also does the same thing; it shows up in module Fraction.hs. Conclusion: when typechecking the methods in a C [a] instance, we want to treat the 'a' as an *existential* type variable, in the sense described by Note [Binding when looking up instances]. That is why isOverlappableTyVar responds True to an InstSkol, which is the kind of skolem we use in tcInstDecl2. }}} In your example, from {{{ instance Run m Int where run = test }}} we get a Wanted `[W] Test m Int` constraint. Because it's in an instance decl, the `m` type variable has the above magic overlap property, we apply the instance declaration to get `[W] (Foo m, Bar m, Baz m)`. I don't say this is great, but I'm not sure what else to do. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12832#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12832: GHC infers too simplified contexts -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by danilo2): @simon, I understand this note (to some degree) and its motivation. In its example it makes perfect sense not to throw an overlap error and compile just fine. But in my example it is just wrong nad I dont see any reason for it (maybe I dont understand something here). Anyway – when I create: {{{ instance Run m Int where run = test }}} It could be possible that I wanted to choose the `Test IM a` as constraint. It could be possible and it would make sense here. Exactly the same sense as the second option available. Why is GHC just blindly choosing one option and throwing a very misguiding error to the user? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12832#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12832: GHC infers too simplified contexts -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): In the Note above there could be two classes that use each other, not just one. I don't have a good solution here, I'm afraid. Maybe someone else does. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12832#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC