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