Re: [GHC] #12553: Reference kind in a type instance declaration defined in another instance declaration

2 Sep 2016

      #12553: Reference kind in a type instance declaration defined in another instance
declaration
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:  TypeInType
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):

 I'll start out by saying that I seem to be missing something!

 == Example that failed in original question ==

 It can be solved by specifying the kind of `a :: Type`:

 {{{#!hs
 -- Compiles fine!
 class Syntactic (a :: Type) where
   type Domain   a :: Sig u -> Type
   type Internal a :: u
   desugar :: a -> ASTF (Domain a) (Internal a)
   sugar   :: ASTF (Domain a) (Internal a) -> a
 }}}

 I believe this to be a bug.

 == I don't know what I'm doing ==

 Replying to [comment:6 simonpj]:
...
Alas Jack has posted no fewer than four different declarations of
 `Internal`, so I'm not sure which one(s) you think should be accepted.
My bad
...
Jack, what kind do you WANT `Internal` to have?
None, possibly! It seems that the kind `u` is an existential kind(?) so
 maybe I should use `DomainInternal` directly, rather than going from `a` →
 `Domain, Internal` → `ASTF (Domain a) (Internal a)`... Or define an
 existential data type that can be converted to `ASTF _ _`.

 {{{#!hs
 data EXISTS where
   EX :: (Sig u -> Type) -> u -> EXISTS

 type family
   ASTify (ex :: EXISTS) :: Type where
   ASTify (EX dom a) = ASTF dom a
 }}}

 Both of these make certain definitions very awkward though, but figuring
 this out is beyond the scope of this ticket.. you go from a neat
 definition like:

 {{{#!hs
 instance Syntactic (a -> b) where
   type Domain   (a -> b) = Domain a
   type Internal (a -> b) = Internal a -> Internal b
 }}}

 to something like this (I believe)

 {{{#!hs
 type family
   DomainInternalArr a b where
   DomainInternalArr (ASTF dom a) (ASTF dom b) = ASTF dom (a -> b)

 instance Syntactic (a -> b) where
   type DomainInternal (a -> b) = DomainInternalArr (DomainInternal a)
 (DomainInternal b)
 }}}

 == Non-solution ==
 Something like this could work if #11962 gets fixed, maybe

 {{{#!hs
 class Syntactic (a :: Type) where
   type SyntKind a :: Type

   type Domain   a :: Sig (SyntKind a) -> Type
   type Internal a :: SyntKind a
 }}}

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