ConstraintKinds inference failure (regression from 7.10)

Posting for a friend who was believed to be spam:

{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

module T where

#if __GLASGOW_HASKELL__ >= 800
import           GHC.Classes (IP(..))
#else
import           GHC.IP (IP(..))
#endif
import           GHC.Exts (Constraint)

-- | From "Data.Constraint":
data Dict :: Constraint -> * where Dict :: a => Dict a
newtype a :- b = Sub (a => Dict b)
infixl 1 \\ -- required comment
(\\) :: a => (b => r) -> (a :- b) -> r
r \\ Sub Dict = r

-- | GHC 7.10.2 type checks this function but GHC 8.0.1 does not unless
-- you modify this example in one of the following ways:
--
--   * uncomments the type signature for 'Sub'
--
--   * flatten the nested pairs of constraints into a triple of constraints
--
--   * replace 'IP sym ty' with 'c9', where 'c9' is a new constraint variable.
--
-- The error message is listed below.
foo :: forall c1 c2 c3 sym ty
    .  (c1, c2) :- c3
    -> (c1, (IP sym ty, c2)) :- (IP sym ty, c3)
foo sp = ( Sub
--           :: ((c1, (IP sym ty, c2)) => Dict (IP sym ty, c3))
--              -> (c1, ((IP sym ty), c2)) :- (IP sym ty, c3)
         )
         ( (Dict \\ sp) :: Dict (IP sym ty, c3) )

{- Compiler error message:

GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling T                ( t.hs, interpreted )

t.hs:44:13: error:
    • Could not deduce: IP sym ty arising from a use of ‘Dict’
      from the context: (c1, (IP sym ty, c2))
        bound by a type expected by the context:
                   (c1, (IP sym ty, c2)) => Dict (IP sym ty, c3)
        at t.hs:(40,10)-(44,49)
      or from: c3
        bound by a type expected by the context:
                   c3 => Dict (IP sym ty, c3)
        at t.hs:44:13-22
    • In the first argument of ‘(\\)’, namely ‘Dict’
      In the first argument of ‘Sub’, namely
        ‘((Dict \\ sp) :: Dict (IP sym ty, c3))’
      In the expression: (Sub) ((Dict \\ sp) :: Dict (IP sym ty, c3))
    • Relevant bindings include
        foo :: (c1, c2) :- c3 -> (c1, (IP sym ty, c2)) :- (IP sym ty, c3)
          (bound at t.hs:40:1)
Failed, modules loaded: none.

-}

Trac metadata

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

changed weight to 5

added Tbug Trac import labels

Trac metadata

Trac field	Value
Operating system	Unknown/Multiple → Linux

Please note: this issue is NOT a blocker for me at present, just something that I happened to notice in passing. Thanks.

changed milestone to %8.0.2

I think this is another manifestation of some bugs in my implementation of recursive superclasses, which was in 8.0. Happily it works just fine in HEAD.

The commit that that may have fixed it is (see #12175 (closed))

commit ce97b7298d54bdfccd9dcf366a69c5617b4eb43f
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Jun 22 14:17:58 2016 +0100

    Expand given superclasses more eagerly

but I have not tested this.

I'm not sure how vigorously we should try to get a fix into 8.0.2, but I'll milestone it as such.

Trac metadata

Trac field	Value
Test case	- → typecheck/should_compile/T12133

mentioned in commit 6cedef01

closed

Indeed the commit mentioned in ticket:12133#comment:122073 has been merged into 8.0.2 and appears to have fixed the issue.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

added Pnormal label