Opened 19 months ago

Closed 19 months ago

Last modified 16 months ago

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

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.

comment:2 Changed 19 months ago by RyanGlScott

#14835 smells similar to this one.

comment:3 Changed 19 months ago by Iceland_jack

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
Last edited 19 months ago by Iceland_jack (previous) (diff)

comment:4 Changed 19 months ago by simonpj

Resolution: fixed
Status: newclosed
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 RyanGlScott

Keywords: wipT2893 removed
Note: See TracTickets for help on using tickets.