Opened 12 months ago

Last modified 8 months ago

#12703 new feature request

Expand Backpack's signature matching relation beyond definitional equality

Reported by: ezyang Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.1
Keywords: backpack Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by ezyang)

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!

One particular place this shows up is if you're incrementally Backpack'ing an interface that has an existing type class. In this case, you might like to just reexport the methods of the type class and "fill" the imports; but these methods have the wrong types! (They're not monomorphic enough).

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.

Change History (2)

comment:1 Changed 8 months ago by ezyang

Description: modified (diff)

comment:2 Changed 8 months ago by ezyang

One of the main technical challenges is extending our declaration merging operation to handle any such subtyping relation.

Note: See TracTickets for help on using tickets.