QuantifiedConstraints: GHC can't deduce (() :: Constraint)?

{-# 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> 

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

mentioned in issue #14835 (closed)

Note that the (:-) part is not needed to trigger this:

{-# 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.

#14835 (closed) smells similar to this one.

Trac metadata

Trac field	Value
Related	- → #14835 (closed)

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

closed

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(-)

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	- → quantified-constraints/T14833

mentioned in issue #14863 (closed)

added 1 deleted label

added Pnormal label