Re: [GHC] #12679: Permit abstract data types in signatures that don't have kind *

13 Oct 2016

      #12679: Permit abstract data types in signatures that don't have kind *
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  low               |            Milestone:
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             Keywords:  backpack
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 ezyang):

 Also, you may be tempted to implement this using a constraint family:

 {{{
     signature Key where
         import GHC.Exts (Constraint)
         type family Key k :: Constraint
         instance Key Bool
 }}}

 But this doesn't work, because GHC expects an instance head to be a type
 class. (This will probably be a problem even if we allow data types that
 are not kind Constraint.) The "silver lining" is that you can just defer
 the "insoluble" constraint to the use-site. But this is terribel, and
 there are other problems too. Here is some code that type checks with
 HEAD, but it is not pretty.

 {{{
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE RoleAnnotations #-}
 unit p where
     signature Key where
         import GHC.Exts (Constraint)
         type family Key :: * -> Constraint
     signature Map where
         import Key
         type role Map nominal representational
         data Map k a
         empty :: Map k a
         insert :: Key k => k -> a -> Map k a -> Map k a
         lookup :: Key k => k -> Map k a -> Maybe a
     module M where
         import Map
         import Key
         -- Need to stick the instance constraint here
         -- (and need to do it explicitly! GHC won't infer it.)
         x :: Key Bool => Map Bool String
         x = insert True "foo" empty
 unit q where
     module Key where
         import GHC.Exts (Constraint)
         type family Key :: * -> Constraint
         type instance Key = Ord
     module Map(Map, M.empty, insert, lookup) where
         import Prelude hiding (lookup)
         import Data.Map (Map)
         import qualified Data.Map as M
         import Key
         -- Ord is NOT definitionally equal to Key, which means
         -- we have to massage the types
         insert :: Key k => k -> a -> Map k a -> Map k a
         insert = M.insert
         lookup :: Key k => k -> Map k a -> Maybe a
         lookup = M.lookup
 unit r where
     dependency p[Key=q:Key, Map=q:Map] -- OK!
 }}}

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