[GHC] #15231: UndecidableInstances validity checking is wrong in the presence of QuantifiedConstraints
#15231: UndecidableInstances validity checking is wrong in the presence of QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 (Type checker) | Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider this program: {{{#!hs {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE QuantifiedConstraints #-} module Bug where import Data.Kind data ECC :: Constraint -> Type -> Type class Y a class Z a instance c => Y (ECC c a) instance (c => Z a) => Z (ECC c a) }}} I would expect both of these instances to work. But while GHC accepts the `Y` instance, it rejects the `Z` instance: {{{ $ ~/Software/ghc5/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:15:10: error: • Variable ‘c’ occurs more often in the constraint ‘c’ than in the instance head (Use UndecidableInstances to permit this) • In the instance declaration for ‘Z (ECC c a)’ | 15 | instance (c => Z a) => Z (ECC c a) | ^^^^^^^^^^^^^^^^^^^^^^^^^ }}} That error message seems completely bogus to me, since `c` appears once in both the context and instance head in both instances. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15231 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15231: UndecidableInstances validity checking is wrong in the presence of QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints 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): GHC is following [https://github.com/Gertjan423/ghc-proposals/blob /quantified-constraints/proposals/0000-quantified-constraints.rst the proposal (Section 3.7)]. Specifically, in the quantified predicate `c => Z a`, `c` does occur more often in the constraint to the left of the arrow, namely `c`, than in the head of the quantified constraint `Z a`. The error message is poor. How about this? {{{ • Variable ‘c’ occurs more often in the constraint ‘c’ than in the instance head `Z a' (Use UndecidableInstances to permit this) • In the quantified constraint `c => Z a` • In the instance declaration for ‘Z (ECC c a)’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15231#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15231: UndecidableInstances validity checking is wrong in the presence of QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints 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 RyanGlScott): Ah, gotcha! That error message does sound like an improvement, yes. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15231#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15231: UndecidableInstances validity checking is wrong in the presence of QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4819 Wiki Page: | -------------------------------------+------------------------------------- Changes (by sighingnow): * status: new => patch * differential: => Phab:D4819 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15231#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15231: UndecidableInstances validity checking is wrong in the presence of
QuantifiedConstraints
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: patch
Priority: normal | Milestone: 8.6.1
Component: Compiler (Type | Version: 8.5
checker) | Keywords:
Resolution: | QuantifiedConstraints
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D4819
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
#15231: UndecidableInstances validity checking is wrong in the presence of QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: fixed | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: quantified- valid program | constraints/T15231 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4819 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => quantified-constraints/T15231 * status: patch => closed * resolution: => fixed * milestone: 8.8.1 => 8.6.1 Comment: Actually, this is //in// GHC 8.6, so this is fixed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15231#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC