Opened 23 months ago

Closed 23 months ago

Last modified 18 months ago

#10742 closed bug (fixed)

GHC cannot deduce (irrelevant) reflexive type equality.

Reported by: ntc2 Owned by:
Priority: normal Milestone: 8.0.1
Component: Compiler (Type checker) Version: 7.10.2
Keywords: TypeLits GADTs Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: polykinds/T10742
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


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.


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

    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.

Change History (7)

comment:1 Changed 23 months ago by thomie

Architecture: x86_64 (amd64)Unknown/Multiple
Operating System: LinuxUnknown/Multiple

Fwiw, ghc HEAD reports:

$ ghc-7.11.20150805 Test.hs
[1 of 1] Compiling TypeLitsBug      ( Test.hs, Test.o )

Test.hs:11:9: warning:
    Redundant constraints: ((x <=? y) ~ 'True, (y <=? z) ~ 'True)
    In the type signature for:
       test :: ((x <=? y) ~ 'True, (y <=? z) ~ 'True) => proxy x y z -> ()

comment:2 Changed 23 months ago by Simon Peyton Jones <simonpj@…>

In 64dba51/ghc:

Test Trac #10742

comment:3 Changed 23 months ago by simonpj

Test Case: polykinds/T10742

Since it works in HEAD, I'm inclined to close this and move on. Unless it is causing real pain that 7.10.2 doesn't work.

I've added a regression test though, to make sure it stays working!


comment:4 Changed 23 months ago by ntc2

We worked around this problem in 7.10.2 so please go ahead and close the issue. I would close it myself, but I'm not sure which of "works in HEAD; please merge" and "close as fixed" to choose for the resolution reason.

comment:5 Changed 23 months ago by simonpj

Resolution: fixed
Status: newclosed

comment:6 Changed 23 months ago by ntc2

In case others run into this, here's a sketch of the workaround.

Define a helper function to discharge the irrelevant constraint:

ghcBugWorkAround :: proxy m n -> ((m <=? n) ~ (m <=? n) => a) -> a
ghcBugWorkAround _ x = x

Wrap the helper around the code which is causing the problem:

f (C ...) = <body> -- Get "can't deduce `m <=? n ~ m <=? n`" error here.


f (C ...) = ghcBugWorkAround <expression fixing m and n> $ <body>

Note that this works even when C ... is a GADT pattern match which brings m or n into scope, in which case you can't simply change the type signature of f to include the m <= n constraint.

Last edited 23 months ago by ntc2 (previous) (diff)

comment:7 Changed 18 months ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.