Opened 2 years ago

Closed 2 years ago

Last modified 2 years 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:

Description

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.

Change History (7)

comment:1 Changed 2 years 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 2 years ago by Simon Peyton Jones <simonpj@…>

In 64dba51/ghc:

Test Trac #10742

comment:3 Changed 2 years 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!

Simon

comment:4 Changed 2 years 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 2 years ago by simonpj

Resolution: fixed
Status: newclosed

comment:6 Changed 2 years 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.

becomes

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 2 years ago by ntc2 (previous) (diff)

comment:7 Changed 2 years ago by thomie

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