#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