[GHC] #10742: GHC cannot deduce (irrelevant) reflexive type equality.
#10742: GHC cannot deduce (irrelevant) reflexive type equality. -------------------------------------+------------------------------------- Reporter: ntc2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 (Type checker) | Keywords: TypeLits | Operating System: Linux GADTs | Architecture: x86_64 | Type of failure: GHC rejects (amd64) | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10742 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10742: GHC cannot deduce (irrelevant) reflexive type equality. -------------------------------------+------------------------------------- Reporter: ntc2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Keywords: TypeLits Resolution: | GADTs Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by thomie): * os: Linux => Unknown/Multiple * architecture: x86_64 (amd64) => Unknown/Multiple Comment: 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 -> () }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10742#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10742: GHC cannot deduce (irrelevant) reflexive type equality.
-------------------------------------+-------------------------------------
Reporter: ntc2 | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 7.10.2
checker) | Keywords: TypeLits
Resolution: | GADTs
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Revisions:
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#10742: GHC cannot deduce (irrelevant) reflexive type equality. -------------------------------------+------------------------------------- Reporter: ntc2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Keywords: TypeLits Resolution: | GADTs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | polykinds/T10742 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => polykinds/T10742 Comment: 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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10742#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10742: GHC cannot deduce (irrelevant) reflexive type equality. -------------------------------------+------------------------------------- Reporter: ntc2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Keywords: TypeLits Resolution: | GADTs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | polykinds/T10742 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10742#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10742: GHC cannot deduce (irrelevant) reflexive type equality. -------------------------------------+------------------------------------- Reporter: ntc2 | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Keywords: TypeLits Resolution: fixed | GADTs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | polykinds/T10742 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10742#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10742: GHC cannot deduce (irrelevant) reflexive type equality. -------------------------------------+------------------------------------- Reporter: ntc2 | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Keywords: TypeLits Resolution: fixed | GADTs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | polykinds/T10742 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by ntc2): In case others run into this, here's a sketch of the workaround. Define a helper function to discharge the irrelevant constraint: {{{#!hs ghcBugWorkAround :: proxy m n -> ((m <=? n) ~ (m <=? n) => a) -> a ghcBugWorkAround _ x = x }}} Wrap the helper around the code which is causing the problem: {{{#!hs f (C ...) = <body> -- Get "can't deduce `m <= n`" error here. }}} becomes {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10742#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC