[GHC] #12787: Weird type constraint with undecidable instances
#12787: Weird type constraint with undecidable instances -------------------------------------+------------------------------------- Reporter: nome | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Linux UndecidableInstances | Architecture: x86_64 | Type of failure: GHC rejects (amd64) | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Minimal example: {{{#!hs {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} module Test where class PreOrd a where (<~) :: a -> a -> Bool class PreOrd a => PartialOrd a where tryCompare :: a -> a -> Maybe Ordering instance PartialOrd a => PreOrd a where x <~ y = let cmp = tryCompare x y in cmp == Just LT || cmp == Just EQ class PartialOrd a => TotalOrd a where tcompare :: a -> a -> Ordering instance TotalOrd a => PartialOrd a where tryCompare x y = Just $ tcompare x y instance TotalOrd Int where tcompare x y = compare x y }}} GHC (tested with 7.10.3 and 8.0.1) rejects this with the following error: {{{ test.hs:11:24: error: • Could not deduce (TotalOrd a) arising from a use of ‘tryCompare’ from the context: PartialOrd a bound by the instance declaration at test.hs:10:10-33 Possible fix: add (TotalOrd a) to the context of the instance declaration • In the expression: tryCompare x y In an equation for ‘cmp’: cmp = tryCompare x y In the expression: let cmp = tryCompare x y in cmp == Just LT || cmp == Just EQ }}} After banging my head against this for a while, and having successfully run this in Hugs, I tend to see it as a bug in GHC. Which is to say, I have no idea why tryCompare could possibly require TotalOrd when it's actually defined in its superclass. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12787 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12787: Weird type constraint with undecidable instances -------------------------------------+------------------------------------- Reporter: nome | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | UndecidableInstances Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This looks like correct behavior to me. There is one, universal instance of `PartialOrd`. As soon as GHC needs the `PartialOrd` constraint to accept the use of `tryCompare`, it will find this instance. But the instance context requires an instance for `TotalOrd`, which does not exist. How would you expect this to be accepted? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12787#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12787: Weird type constraint with undecidable instances -------------------------------------+------------------------------------- Reporter: nome | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | UndecidableInstances Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by nome): Maybe I've minimized the example a bit too much. The `PartialOrd` instance given is not meant to be universal, but as a default. In a slightly more realistic example, it would be made overlappable, like so: {{{#!hs instance {-# OVERLAPPABLE #-} TotalOrd a => PartialOrd a where tryCompare x y = Just $ tcompare x y }}} And there would be additional instances, e.g. {{{#!hs import Data.List -- insert classes and instances as above instance Eq a => PartialOrd [a] where tryCompare xs ys = if xs == ys then Just EQ else if null (xs \\ ys) then Just LT else if null (ys \\ xs) then Just GT else Nothing }}} If I understand [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... #instance-overlap overlapping instances] correctly, GHC should consider ''all'' applicable instances and be "conservative about committing to an overlapping instance", so I would expect it to refrain from committing to the `TotalOrd a => PartialOrd a` one. Still, even with these additions, I get the same error. Ideally, the default implementation would be part of the `PartialOrd` class (like default implementations of the class's own methods); but it seems that there's no way to provide default implementations for superclass methods in a class declaration. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12787#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12787: Weird type constraint with undecidable instances -------------------------------------+------------------------------------- Reporter: nome | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: invalid | UndecidableInstances Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by nome): * status: new => closed * resolution: => invalid Comment: After some more head banging and scratching, I'm heading towards the conclusion that I simply can't use the context of an instance declaration to put a restriction on the types it applies to. It looks like it should be possible in principle, but if that's not how the language works, there's little point in arguing. Unlike the minimal example, the extended one given above doesn't work in Hugs either. I'm still not entirely sure about all of this stuff, particularly the overlapping instances bit, but it appears that the bug was really in my interpretation. Sorry for the noise... I've never met a language that's both so beautiful and so liable to tying knots into my brain. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12787#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12787: Weird type constraint with undecidable instances -------------------------------------+------------------------------------- Reporter: nome | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: invalid | UndecidableInstances Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): No worries about the noise -- and sorry if my initial response was a bit curt. This is confusing territory to be sure! For me, the key that unlocked all of this was to realize that instance selection always ignores contexts. So GHC will choose an instance based only on the instance head (that is, the bit to the right of `=>`). Only then will it try to satisfy the context. More elaborate instance selection control is possible with type families, but I'm afraid I can't find a decent, introductory example of how to do this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12787#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12787: Weird type constraint with undecidable instances -------------------------------------+------------------------------------- Reporter: nome | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: invalid | UndecidableInstances Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by nome): Thank you for the explanations. For the record: After some more reading (and a lot more thinking) on this topic, I realize that a) type classes are much weirder than I thought, and that b) the language and syntax of contexts is pretty misleading. It looks as though they're something like type-level guards (i.e. a precondition), but they're really constraints on polymorphic types ''resulting'' from applying a type class to a type: {{{#!hs type family constraintPartOfPartialOrd a :: Constraint type instance constraintPartOfPartialOrd a = TotalOrd a type instance constraintPartOfPartialOrd [a] = Eq a }}} ... put like this, it's clear why the deduced constraint is always `TotalOrd a`. So the instance syntax is really the wrong way around, and should instead be something like {{{#!hs instance PartialOrd a = TotalOrd a => tryCompare x y = Just $ tcompare x y }}} or maybe {{{#!hs instance PartialOrd a where type constraint TotalOrd a tryCompare x y = Just $ tcompare x y }}} because constraints are "attached" to the value-level part of a type class instance in pretty much the same way as [https://wiki.haskell.org/GHC/Type_families#An_associated_type_synonym_exampl... associated type synonyms]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12787#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC