Re: [GHC] #6018: Injective type families

15 May 2014

      #6018: Injective type families
-------------------------------+-------------------------------------------
        Reporter:  lunaris     |            Owner:  simonpj
            Type:  feature     |           Status:  new
  request                      |        Milestone:  7.10.1
        Priority:  normal      |          Version:  7.4.1
       Component:  Compiler    |         Keywords:  TypeFamilies, Injective
      Resolution:              |     Architecture:  Unknown/Multiple
Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple             |       Blocked By:
 Type of failure:              |  Related Tickets:  #4259
  None/Unknown                 |
       Test Case:              |
        Blocking:              |
-------------------------------+-------------------------------------------

Comment (by spacekitteh):

 Here's another real world use case.

 Given

 {{{
 class Manifold' a where
     type Field a
     type Base  a
     type Tangent a
     type TangentBundle a
     type Dimension a∷  Nat
     type UsesMetric a∷ Symbol
     project ∷ a → Base a
     unproject ∷ Base a→ a
     tangent ∷ a → TangentBundle a
     cotangent ∷ a → (TangentBundle a→ Field a)
 }}}

 then this works:
 {{{
 id' ∷ ∀ a. ( Manifold' a) ⇒ Base a → Base a
 id' input= project out where
     out∷a
     out = unproject input
 }}}

 whereas this requires injective type families:

 {{{
 id' ∷ ∀ a. ( Manifold' a) ⇒ Base a → Base a
 id' = project ∘ unproject
 }}}

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