[GHC] #12551: Make type indices take local constraints into account in type instance declaration

[GHC]

#12551: Make type indices take local constraints into account in type instance
declaration
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

@@ -7,2 +7,2 @@
-   Full  :: a      -> Sig a
-   (:->) :: a -> b -> Sig a
+   Full  :: a          -> Sig a
+   (:->) :: a -> Sig a -> Sig a

New description:

 Given

 {{{#!hs
 infixl 1 :$
 infixr :->
 data Sig x where
   Full  :: a          -> Sig a
   (:->) :: a -> Sig a -> Sig a

 data AST dom a where
   Sym  :: dom a -> AST dom a
   (:$) :: AST dom (a:->b) -> AST dom (Full a) -> AST dom b

 class Syntactic a dom | a -> dom where
   type Rep a
   desugar :: a -> AST dom (Full (Rep a))
   sugar   :: AST dom (Full (Rep a)) -> a
 }}}

 I want to be able to define the trivial instance for `Syntactic (AST dom
 (Full a))`:

 {{{#!hs
 instance Syntactic (AST dom (Full a)) dom where
   type Rep (AST dom (Full a)) = a
   desugar, sugar :: AST dom (Full a) -> AST dom (Full a)
   desugar = id
   sugar   = id
 }}}

 This should be the only `Syntactic` instance for `AST _ _` so I would like
 to apply the [http://chrisdone.com/posts/haskell-constraint-trick
 ‘constraint’ trick]
 ([https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025d9da2a70
 #blog-reddit-constraint-trick-for-instances link]) but I cannot use the
 `Rep` instance as before:

 {{{#!hs
 --     • Type indexes must match class instance head
 --       Found ‘AST dom ('Full a)’ but expected ‘AST dom full_a’
 --     • In the type instance declaration for ‘Rep’
 --       In the instance declaration for ‘Syntactic (AST dom full_a) dom’

 instance full_a ~ Full a => Syntactic (AST dom full_a) dom where
   type Rep (AST dom (Full a)) = a
 }}}

 Maybe this could be accepted, given that `full_a ~ Full a`, therefore the
 instance head is equal to `AST dom (Full a)`?

 My current workaround is using a type family

 {{{#!hs
 type family
   Edrú a where
   Edrú (Full a) = a

 instance full_a ~ Full a => Syntactic (AST dom full_a) dom where
   type Rep (AST dom full_a) = Edrú full_a
   desugar, sugar :: AST dom (Full a) -> AST dom (Full a)
   desugar = id
   sugar   = id
 }}}

--

Comment (by Iceland_jack):

 Replying to [ticket:12551 Iceland_jack]:
 > Given
 >
 > {{{#!hs
 > infixl 1 :$
 > infixr :->
 > data Sig x where
 >   Full  :: a      -> Sig a
 >   (:->) :: a -> b -> Sig a
 >
 > data AST dom a where
 >   Sym  :: dom a -> AST dom a
 >   (:$) :: AST dom (a:->b) -> AST dom (Full a) -> AST dom b
 >
 > class Syntactic a dom | a -> dom where
 >   type Rep a
 >   desugar :: a -> AST dom (Full (Rep a))
 >   sugar   :: AST dom (Full (Rep a)) -> a
 > }}}
 >
 > I want to be able to define the trivial instance for `Syntactic (AST dom
 (Full a))`:
 >
 > {{{#!hs
 > instance Syntactic (AST dom (Full a)) dom where
 >   type Rep (AST dom (Full a)) = a
 >   desugar, sugar :: AST dom (Full a) -> AST dom (Full a)
 >   desugar = id
 >   sugar   = id
 > }}}
 >
 > This should be the only `Syntactic` instance for `AST _ _` so I would
 like to apply the [http://chrisdone.com/posts/haskell-constraint-trick
 ‘constraint’ trick]
 ([https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025d9da2a70
 #blog-reddit-constraint-trick-for-instances link]) but I cannot use the
 `Rep` instance as before:
 >
 > {{{#!hs
 > --     • Type indexes must match class instance head
 > --       Found ‘AST dom ('Full a)’ but expected ‘AST dom full_a’
 > --     • In the type instance declaration for ‘Rep’
 > --       In the instance declaration for ‘Syntactic (AST dom full_a)
 dom’
 >
 > instance full_a ~ Full a => Syntactic (AST dom full_a) dom where
 >   type Rep (AST dom (Full a)) = a
 > }}}
 >
 > Maybe this could be accepted, given that `full_a ~ Full a`, therefore
 the instance head is equal to `AST dom (Full a)`?
 >
 > My current workaround is using a type family
 >
 > {{{#!hs
 > type family
 >   Edrú a where
 >   Edrú (Full a) = a
 >
 > instance full_a ~ Full a => Syntactic (AST dom full_a) dom where
 >   type Rep (AST dom full_a) = Edrú full_a
 >   desugar, sugar :: AST dom (Full a) -> AST dom (Full a)
 >   desugar = id
 >   sugar   = id
 > }}}

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