[GHC] #14833: QuantifiedConstraints: GHC can't deduce (() :: Constraint)?
#14833: QuantifiedConstraints: GHC can't deduce (() :: Constraint)? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints wipT2893 | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs #-} import Data.Kind data Dict c where Dict :: c => Dict c class (a => b) => Implies a b instance (a => b) => Implies a b type a :- b = Dict (Implies a b) iota :: (Implies () a) :- a iota = Dict }}} GHC claims that it can't deduce `(() :: Constraint)` :) {{{ GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/H.hs, interpreted ) /tmp/H.hs:14:8: error: • Could not deduce () :: Constraint arising from a use of ‘Dict’ from the context: Implies () :: Constraint a bound by a quantified context at /tmp/H.hs:1:1 Possible fix: add () :: Constraint to the context of the type signature for: iota :: forall (a :: Constraint). Implies () :: Constraint a :- a • In the expression: Dict In an equation for ‘iota’: iota = Dict | 14 | iota = Dict | ^^^^ Failed, no modules loaded. Prelude> }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14833 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14833: QuantifiedConstraints: GHC can't deduce (() :: Constraint)? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Note that the `(:-)` part is not needed to trigger this: {{{#!hs {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE UndecidableInstances #-} module Bug where data Dict c where Dict :: c => Dict c class (a => b) => Implies a b instance (a => b) => Implies a b iota1 :: (() => a) => Dict a iota1 = Dict iota2 :: Implies () a => Dict a iota2 = Dict }}} Note that `iota1` typechecks but `iota2` does not. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14833#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14833: QuantifiedConstraints: GHC can't deduce (() :: Constraint)? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14835 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #14835 Comment: #14835 smells similar to this one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14833#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14833: QuantifiedConstraints: GHC can't deduce (() :: Constraint)? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14835 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Same as? {{{#!hs {-# Language QuantifiedConstraints, GADTs, FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, UndecidableInstances #-} import Data.Kind import Data.Proxy import Unsafe.Coerce data Dict c where Dict :: c => Dict c class (a => b) => Entails a b instance (a => b) => Entails a b wit :: Dict a -> Dict b -> Dict (Entails (a, b) xx) -> Dict xx wit Dict Dict Dict = Dict }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14833#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14833: QuantifiedConstraints: GHC can't deduce (() :: Constraint)?
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler | Version: 8.5
Resolution: fixed | Keywords:
| QuantifiedConstraints wipT2893
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case: quantified-
| constraints/T14833
Blocked By: | Blocking:
Related Tickets: #14835 | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Changes (by simonpj):
* testcase: => quantified-constraints/T14833
* status: new => closed
* resolution: => fixed
Comment:
I've fixed this one -- on `wip/T2893` as always.
==
{{{
commit 60f682407eefdb7884d12ba43d00add0c1ca9245
Author: Simon Peyton Jones
participants (1)
-
GHC