#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_constraint... 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