Re: [GHC] #9131: Experiment with a dedicated solver for Coercible

21 May 2014

      #9131: Experiment with a dedicated solver for Coercible
-------------------------------------+------------------------------------
        Reporter:  nomeata           |            Owner:
            Type:  task              |           Status:  new
        Priority:  low               |        Milestone:
       Component:  Compiler          |          Version:  7.8.2
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Comment (by nomeata):
...
What are the theoretical properties of solving Coercible constraints? Is
 it even decidable? Semi decidable? Are there existing standard algorithms?
 How does this relate to SMT solving? And why don’t I know these things...
Pondering this a bit, I think it is unsolvable, as we can encode the
 problem of whether two simply typed lambda terms with fix are equivalent.
 (It’s simply typed because our types are kinded).

 For `fix :: (* -> *) -> *`, we need
 {{{
 newtype Fix1 f = Fix1 (f (Fix1 f))
 }}}
 (and similar code for `fix` at higher types).

 So given a lambda expression, we do full lambda lifting to give the
 lambdas names, eta-expand according to their type and turn them into
 newtypes.

 {{{
 module Lambda where

 import Data.Coerce

 newtype Fix1 f   = Fix1 (f (Fix1 f))
 newtype Fix2 f x = Fix2 (f (Fix2 f) x)

 -- lambda terms
 -- a = λ f. λ y. f (f y)        :: (* -> *) -> * -> *
 -- b = λ f. λ y. fix (λ x. f x) :: (* -> *) -> * -> *

 -- lambda lifted
 -- a1 f y = f (f y)
 -- a f = a1 f

 -- b1 f x = f x
 -- b2 f y = fix (b1 f)
 -- b f = b2 f

 -- The newtypes

 newtype A1 f y = A1 (f (f y))
 newtype A y x  = A  (A1 y x)

 newtype B1 f x = B1 (f x)
 newtype B2 f y = B2 (Fix1 (B1 f))
 newtype B f x  = B  (B2 f x)

 -- Querying equivalence (Passing types with representational arguments as
 -- parameters so that the solver doesn't stop at `Coercible (f ...) (f
 ...)`

 ex :: A Maybe () -> B Maybe ()
 ex = coerce
 }}}

 This is not fully worked out yet, but it seems to be reasonable to assume
 that our `Coercible` solver will never be complete and we’ll live with
 some shortcomings anyways.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9131#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler