[GHC] #10742: GHC cannot deduce (irrelevant) reflexive type equality.

[GHC]

#10742: GHC cannot deduce (irrelevant) reflexive type equality.
-------------------------------------+-------------------------------------
              Reporter:  ntc2        |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.2
  (Type checker)                     |
              Keywords:  TypeLits    |  Operating System:  Linux
  GADTs                              |
          Architecture:  x86_64      |   Type of failure:  GHC rejects
  (amd64)                            |  valid program
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:
Differential Revisions:              |
-------------------------------------+-------------------------------------
 GHC is creating an irrelevant reflexive type equality and then failing to
 deduce it. The problem seems to be related to transitivity for
 `GHC.TypeLits.Nat`, as the example will make clear.

 Example:
 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeOperators #-}

 module TypeLitsBug where

 import GHC.TypeLits

 data T a where MkT :: T Int

 test :: ((x <=? y) ~ 'True, (y <=? z) ~ 'True)
      => proxy x y z -> ()
 test _ = case MkT of MkT -> ()
 }}}

 Error message:
 {{{
 $ ghc --version
 The Glorious Glasgow Haskell Compilation System, version 7.10.2

 $ ghc -c TypeLitsBug.hs

 TypeLitsBug.hs:11:9:
     Could not deduce ((x <=? z) ~ (x <=? z))
     from the context ((x <=? y) ~ 'True, (y <=? z) ~ 'True)
       bound by the type signature for
                  test :: ((x <=? y) ~ 'True, (y <=? z) ~ 'True) => proxy x
 y z -> ()
       at TypeLitsBug.hs:(11,9)-(12,25)
     NB: ‘<=?’ is a type function, and may not be injective
 }}}

 Notice the `x <=? z` relating `x` to `z`. I only mention `x <=? y` and `y
 <=? z` in the program, so it seems transitivity of `<=` is implicitly
 involved. Also, the problem goes away if I remove the GADT pattern match.

 I asked Iavor about this and he suspected the ambiguity check.

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