#14833 closed bug (fixed)
QuantifiedConstraints: GHC can't deduce (() :: Constraint)?
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.5 |
Keywords: | QuantifiedConstraints | Cc: | |
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: |
Description
{-# 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>
Change History (5)
comment:1 Changed 19 months ago by
comment:3 Changed 19 months ago by
Same as?
{-# 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
or
pair :: Dict (Entails xx a) -> Dict (Entails xx b) -> Dict (Entails xx (a, b)) pair Dict Dict = Dict
comment:4 Changed 19 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → quantified-constraints/T14833 |
I've fixed this one -- on wip/T2893
as always.
commit 60f682407eefdb7884d12ba43d00add0c1ca9245 Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Tue Feb 27 13:43:26 2018 +0000 Fix a bunch of buglets in QuantifiedConstraints * Freshen tyvars in Inst.instDFunType * Freshen tyvars in TcCanonical.solveForAll * Define TcSMonad.mightMatchLater, and use it (fixes Trac #14833) * Add testsuite directry tests/quantified-constraints/, and start to populate it compiler/typecheck/Inst.hs | 8 ++++++-- compiler/typecheck/TcCanonical.hs | 22 ++++++++++++++-------- compiler/typecheck/TcEvidence.hs | 2 -- compiler/typecheck/TcInteract.hs | 34 ++++++++++++++++------------------ compiler/typecheck/TcSMonad.hs | 21 +++++++++++---------- compiler/typecheck/TcValidity.hs | 3 ++- compiler/types/Type.hs | 2 +- testsuite/tests/quantified-constraints/T14833.hs | 28 ++++++++++++++++++++++++++++ testsuite/tests/quantified-constraints/T2893.hs | 18 ++++++++++++++++++ testsuite/tests/quantified-constraints/T2893a.hs | 27 +++++++++++++++++++++++++++ testsuite/tests/quantified-constraints/T2893b.hs | 24 ++++++++++++++++++++++++ testsuite/tests/quantified-constraints/all.T | 4 ++++ testsuite/tests/typecheck/should_compile/T2893.hs | 18 ------------------ testsuite/tests/typecheck/should_compile/T2893a.hs | 27 --------------------------- testsuite/tests/typecheck/should_compile/all.T | 2 -- 15 files changed, 151 insertions(+), 89 deletions(-)
comment:5 Changed 16 months ago by
Keywords: | wipT2893 removed |
---|
Note: See
TracTickets for help on using
tickets.
Note that the
(:-)
part is not needed to trigger this:Note that
iota1
typechecks butiota2
does not.