GHC cannot deduce (irrelevant) reflexive type equality.

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:

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

Trac metadata

Trac field	Value
Version	7.10.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system	Linux
Architecture	x86_64 (amd64)