[GHC] #12703: Expand Backpack's signature matching relation beyond definitional equality

[GHC]

#12703: Expand Backpack's signature matching relation beyond definitional equality
-------------------------------------+-------------------------------------
           Reporter:  ezyang         |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:  backpack       |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Currently, signature matching is done by strict definitional equality.
 This can be pretty inconvenient in some cases (it is also the only place
 in the Haskell language that we actually expose definitional equality):

 **Polymorphism.** This is the obvious one. If I have an implementing
 function that is more polymorphic than my signature, I have to manually
 monomorphize it.

 {{{
 unit p where
     signature H where
         import Prelude (Int)
         data String
         length :: String -> Int

 unit q where
     module H(String, length) where
         -- from Prelude

 unit r where
     dependency p[H=q:H]
 }}}

 Gives

 {{{
 <no location info>: error:
     Identifier ‘Data.Foldable.length’ has conflicting definitions in the
 module
     and its hsig file
     Main module: Data.Foldable.length ::
                    Data.Foldable.Foldable t => forall a. t a ->
 GHC.Types.Int
     Hsig file:  Data.Foldable.length ::
                   GHC.Base.String -> GHC.Types.Int
     The two types are different
 }}}

 Essentially, you have to monomorphize any functions you want to use.
 Annoying!

 **Quantifier ordering.** Here's a more subtle one: if I don't explicitly
 specify a type signature, GHC will pick whatever quantifier ordering it
 wants. Quantifier ordering affects definitional equality.

 It's actually pretty easy to trigger this, since GHC seems to always pick
 the reverse of what you'd get if you explicitly specified the type
 signature:

 {{{
 unit p where
     signature H where
         k :: a -> b -> a

 unit q where
     module H where
         k x y = x

 unit r where
     dependency p[H=q:H]
 }}}

 Fails with:

 {{{
 q.bkp:7:9: error:
     Identifier ‘q:H.k’ has conflicting definitions in the module
     and its hsig file
     Main module: q:H.k :: t2 -> t1 -> t2
     Hsig file:  q:H.k :: a -> b -> a
     The two types are different
 }}}

 **Constraint relaxation.** In #12679, you might want to define an abstract
 class which you can use to let implementors pass in type class instances
 that they might need. But you often end up in situations where the real
 implementations of your functions require less constraint than the
 signature specifies; for example, you might write `insert :: Key k => k ->
 a -> Map k a -> Map k a`, but if Map is an association list and just
 appends the new value onto the front of the list, no Eq constraint needed!
 There goes another impedance matching binding.

 **Type families.** Type family applications aren't reduced when deciding
 definitional equality.

 {{{
 {-# LANGUAGE TypeFamilies #-}
 unit p where
     signature H where
         f :: Int

 unit q where
     module H where
         type family F
         type instance F = Int
         f :: F
         f = 2

 unit r where
     dependency p[H=q:H]
 }}}

 Gives

 {{{
 q.bkp:11:9: error:
     Identifier ‘q:H.f’ has conflicting definitions in the module
     and its hsig file
     Main module: q:H.f :: q:H.F
     Hsig file:  q:H.f :: GHC.Types.Int
     The two types are different
 }}}

 **Discussion.** It's instructive to consider what the impacts of this sort
 of relaxation would have on hs-boot files. Some of the equalities that
 users expect in the source language have operational impact: for example,
 the ordering of constraints affects the calling convention of the function
 in question. So there would need to be an impedance matching binding to
 reorder/drop constraints to match the defining function. We already do an
 impedance matching of this sort with dictionary functions; this would be a
 logical extension. Thus, a signature would have to monomorphize, coerce,
 etc--whatever it needs to show the matching holds. I think this is quite
 plausible, although it would require rewriting this chunk of code.

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