[GHC] #2256: Incompleteness of type inference: must quantify over implication constraints

[GHC]

#2256: Incompleteness of type inference: must quantify over implication
constraints
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  simonpj
            Type:  bug               |               Status:  new
        Priority:  lowest            |            Milestone:
       Component:  Compiler (Type    |              Version:  6.8.2
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 From [http://arxiv.org/pdf/1511.09394v1.pdf Proof Relevant Corecursive
 Resolution], I will copy the relevant text:

 > Derivable type classes.:::
 >
 > Hinze and Peyton Jones wanted to use an instance of the form
 >
 > {{{#!hs
 > instance (Binary a, Binary (f (GRose f a))) => Binary (GRose  f a)
 > }}}
 >
 > but discovered that it causes resolution to diverge. They suggested the
 following as a replacement:
 >
 > {{{#!hs
 > instance (Binary a, ∀b. Binary b => Binary (f b)) => Binary (GRose f a)
 > }}}
 >
 > Unfortunately, Haskell does not support instances with ''polymorphic
 higher-order instance contexts''. Nevertheless, allowing such implication
 constraints would greatly increase the expressivity of corecursive
 resolution. In the terminology of our paper, it amounts to extending Horn
 formulas to intuitionistic formulas. Working with intuitionistic formulas
 would require a certain amount of searching, as the non-overlapping
 condition for Horn formulas is not enough to ensure uniqueness of the
 evidence. For example, consider the following axioms:
 >
 > {{{
 > κ₁ : (A ⇒ B x) ⇒ D (S x)
 > ĸ₂ : A, D x ⇒ B (S x)
 > κ₃ : ⇒ D Z
 > }}}
 > We have two distinct proof terms for `D (S (S (S (S Z)))))`:
 >
 > {{{
 > κ₁ (λα₁. ĸ₂ α₁ (ĸ₁ (λα₂. ĸ₂ α₁ ĸ₃))
 > κ₁ (λα₁. ĸ₂ α₁ (ĸ₁ (λα₂. ĸ₂ α₂ ĸ₃))
 > }}}
 >
 > This is undesirable from the perspective of generating evidence for type
 class.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/2256#comment:25>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler