id summary reporter owner description type status priority milestone component version resolution keywords cc os architecture failure testcase blockedby blocking related differential wikipage
10742 GHC cannot deduce (irrelevant) reflexive type equality. ntc2 "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." bug closed normal 8.0.1 Compiler (Type checker) 7.10.2 fixed TypeLits GADTs Unknown/Multiple Unknown/Multiple GHC rejects valid program polykinds/T10742