[GHC] #12133: ConstraintKinds inference failure (regression from 7.10)

[GHC]

#12133: ConstraintKinds inference failure (regression from 7.10)
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Posting for a friend who was believed to be spam:

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

 -}
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12133>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler