#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