[GHC] #14878: Can't witness transitivity ((.)) of isomorphism of Constraints

[GHC]

#14878: Can't witness transitivity ((.)) of isomorphism of Constraints
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.5
      Resolution:  invalid           |             Keywords:
                                     |  QuantifiedConstraints, wipT2893
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by Iceland_jack):

 * status:  new => closed
 * resolution:   => invalid


Comment:

 Ah that's sensible, and not too difficult to work around:

 {{{#!hs
 {-# Language QuantifiedConstraints, GADTs, ConstraintKinds, TypeOperators,
 FlexibleInstances, MultiParamTypeClasses, UndecidableInstances,
 TypeApplications, ScopedTypeVariables #-}

 import Data.Kind

 data Dict c where
   Dict :: c => Dict c

 class    (a => b) => Implies a b
 instance (a => b) => Implies a b

 type a  :- b = Dict (Implies a b)
 type a -:- b = Dict (Implies a b, Implies b a)

 type Iso s t a b = Dict (Implies a b, Implies s t)

 comp_ :: forall a b c. a-:-b -> b-:-c -> a-:-c
 comp_ Dict Dict = comp__ @c @b @a @b @a @c b1 a1 a2 b2 where

   a1 :: a:-b
   a1 = Dict

   a2 :: b:-a
   a2 = Dict

   b1 :: c:-b
   b1 = Dict

   b2 :: b:-c
   b2 = Dict

 comp__ :: s:-t -> a:-b -> t:-i -> b:-c -> Iso s i a c
 comp__ Dict Dict Dict Dict = Dict
 }}}

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