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

11 Jul 2016

      ...
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
#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:

 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

GHC

tags

participants (1)