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

29 Aug 2016

      #12551: Make type indices take local constraints into account in type instance
declaration
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:  TypeFamilies   |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler