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

Architecture: | x86_64 (amd64) → Unknown/Multiple |
---|---|

Operating System: | Linux → Unknown/Multiple |

### comment:3 Changed 2 years ago by

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

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

Resolution: | → fixed |
---|---|

Status: | new → closed |

### comment:6 Changed 2 years ago by

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.

### comment:7 Changed 2 years ago by

Milestone: | → 8.0.1 |
---|

**Note:**See TracTickets for help on using tickets.

Fwiw, ghc HEAD reports: