#12466: Typechecker regression: Inaccessible code in a type expected by the context -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.1 checker) | 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 ekmett): I think there is morally a difference between {{{#!hs class Foo a where foo :: (a ~ Int => a) -> a -> a }}} and your example which is more like {{{#!hs class Foo a where foo :: (a ~ Int) => a -> a -> a }}} in terms of if we should reject things once we know `a ~ Char`, and that hence `a ~ Int` can never happen. In the former you're given two arguments, one of which requires you to provide something impossible to use, and so simply cant be used, while in the latter you're required to implement a contradiction when you go to write `instance Foo Char`. Notice the polarity of the equality constraint. In the former it is in positive position. In the latter it is in negative position as usual. Finding a contradiction in negative position fits with Richard's intuition about if we should complain, but in positive position it simply means that argument is inaccessible, which is perfectly okay. Someone might pass it in in a more polymorphic setting where they don't know if the constraint could be satisfied or not, until the instance for Foo is selected, which is what is happening here. Today I usually hack around the latter by passing an explicit Dict for the constraint, so that I have the option to bring it into scope or not, and can carefully avoid GHC prematurely detonating upon discovering the contradiction {{{#!hs class Foo a where foo :: Dict (a ~ Int) -> a -> a -> a }}} but until now I haven't had to hack around it for the former -- and the explicit Dict-based solutions are much clunkier to both write, and for users to use in practice. (We used to use this approach to implement ex falso quodlibet in the `constraints` package, but now we just use `Any` directly as an uninhabitable initial `Constraint`.)
Currently
{{{#!hs foo :: (Char ~ Int => Int) -> a -> a foo _ a2 = a2 }}}
gives a similar message. Is that reasonable? The argument to foo can't be called.
I'd personally think that that should be allowed, as silly as it looks in this very concrete case. `foo` itself doesn't care about the argument at all. The burden of complaining about the impossibility of what we can see locally would be `Int ~ Char` should fall on type checking the argument passed to `foo` at the call site, not to `foo`, and at that call site it may or may not be impossible as it may not know the `Int` part of the equation there. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12466#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler