[GHC] #14362: Allow: Coercing (a:~:b) to (b:~:a)

[GHC]

#14362: Allow: Coercing (a:~:b) to (b:~:a)
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:  roles
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 Is it not ultimately about implication of constraints
 ([https://www.reddit.com/r/haskell/comments/6me3sv/quantified_class_constraints_pdf/
 quantified constraints])

 {{{#!hs
 -- Witness Constraint
 data Dict :: Constraint -> Type where
   Dict :: ctx => Dict ctx

 instance (ctx           => ctx')            => Coercible (Dict ctx)
 (Dict ctx')
 instance (Coercible a b => Coercible a' b') => Coercible (Coercion a b)
 (Coercion a' b')
 instance ((a ~ b)       => (a' ~ b'))       => Coercible (a:~:b)
 (a':~:b')
 }}}

 In the case of symmetry,

 * To `coerce :: a:~:b -> b:~:a` we need to show
   * `a ~ b => b ~ a`
 * To `coerce :: Coercion a b -> Coercion b a` we need to show
   * `Coercible a b => Coercible b a`

 If we think of the class of data types witnessing an `Underlying`
 constraint

 {{{#!hs
 type family
   ToConstraint (kind :: Type) = (res :: Type) | res -> kind where
   ToConstraint Type     = Constraint
   ToConstraint (a -> b) = a -> ToConstraint b

 type family
   Underlying (dataty :: kind) :: ToConstraint kind where
   Underlying (Dict ctx) = ctx

   Underlying Coercion   = Coercible
   Underlying (:~:)      = (~)
   Underlying (:~~:)     = (~~)
 }}}

 we can could write these in a more general form:

 {{{#!hs
 instance (Underlying thing     => Underlying thing')       => Coercible
 thing       thing'
 instance (Underlying thing a   => Underlying thing' a')    => Coercible
 (thing a)   (thing' a')
 instance (Underlying thing a b => Underlying thing' a' b') => Coercible
 (thing a b) (thing' a' b')
 }}}

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