#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