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

29 Aug 2016


      ...
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
#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]:
 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

    