Re: [GHC] #8423: contraint solver doesn't reduce reducible closed type family expressions (even with undecidable instances!)

9 Oct 2013

      #8423: contraint solver doesn't  reduce reducible closed type family expressions
(even with undecidable instances!)
--------------------------------------------+------------------------------
        Reporter:  carter                   |            Owner:
            Type:  feature request          |           Status:  new
        Priority:  normal                   |        Milestone:  7.10.1
       Component:  Compiler (Type checker)  |          Version:  7.7
      Resolution:                           |         Keywords:
Operating System:  Unknown/Multiple         |     Architecture:
 Type of failure:  None/Unknown             |  Unknown/Multiple
       Test Case:                           |       Difficulty:  Unknown
        Blocking:                           |       Blocked By:
                                            |  Related Tickets:  #4259
--------------------------------------------+------------------------------

Comment (by carter):

 excellent points that i probably agree with (and i'll have to dig into
 that other ticket as time permits)

 Hrm, another way of looking at it is that i'd be ok with having to come up
 with sort of induction principles or the like that let me give the type
 checker the proofs! Currently we dont have a decent story that plays well
 with equality constraints.

 so I either need to "lie about the types" and do something like

 {{{

 reverseShape :: Shape r -> Shape r
 reverseShape Nil = Nil
 reverseShape shs@(anIx :* rest) = go  shs Nil
     where
       --- too weakly typed
         go ::  Shape a -> Shape b -> Shape r -- want r= PSum a b
         go  Nil res =  unsafeCoerce $  res   -- 0 + b = b ==> b=r
         go (ix :* more )  res =  go more  (ix :* res) --- 1+a + b = r
 }}}

 (which has a cast in the base case, but is ok othewise)

 OR try to have some sort of "proof" mapping, which honestly dones't work,
 and to even "write" the terms required
 {{{
 {-# LANGUAGE AllowAmbiguousTypes #-}
 }}}

 that attempt looked like the following
 {{{
 assocSumSucc :: Shape (PSum ('S r2) b) -> Shape ( PSum r2 ('S b))
 assocSumSucc = unsafeCoerce

 assocSumSuccBad :: Shape (PSum a b) -> Shape ( PSum c  d)
 assocSumSuccBad = unsafeCoerce
 }}}
 this doesn't quite work, because neither interacts with the equality
 constraint solving!

 So the only sane thing of that sort is

 {{{
 shapeCoerce :: Shape a -> Shape b
 shapeCoerce = unsafeCoerce
 }}}
 which is honestly  pretty bad!  (and apply this in the recursive case)

 these as all (unlike the other solution inline above) pretty bad, because
 they break tail calls.

 I guess what i want is a way have having "proof principles" or something
 that i could build, which would interact well with the types.

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