GHC+DH Weekly Update #2, 2022-12-21

#1

Hi all, here’s another update on the implementation of dependent types in GHC.

This time I worked on solving an issue with visibility of type variables. In GHC, a forall-bound variable may have one of the three visibilities:

  • required, written forall a ->
  • specified, written forall a.
  • inferred, written forall {a}.

This distinction is important in surface Haskell, but it does not make any difference in Core. So in an ideal world, we would be careful to track it in the type checker and discard it afterwards. At the moment, however, GHC does neither. The current design is to play fast and loose with the specified vs inferred distinction, but be strict about required vs non-required variables. This results in the worst of both worlds:

  1. in Core, we can not use lambdas to bind required variables
  2. in Haskell, we can accidentally write programs that rely on the implementation details of GHC’s kind inference engine

The first issue is what drew my attention to this. In fact, it is a blocker for MR !9257, so it needs to be addressed to make progress on dependent types. The second issue, however, also deserves some attention, and I opened #22648 to track it.

Fortunately, we can kill two birds with one stone if we implement visibility subsumption. The idea is as follows:

  1. Ignore visibility of forall-bound variables in eqType and tcEqType completely.

  2. Define a subsumption relation between the expected and actual ForAllTyFlag:

    sub_vis :: ForAllTyFlag -> ForAllTyFlag -> Bool
sub_vis Specified Inferred = True
sub_vis flag1     flag2    = flag1 == flag2

  3. Define a new check tcSubVis:

    tcSubVis
  :: Type     -- actual
  -> Type     -- expected
  -> Bool
    • In Core Lint, do not use it.
    • In Haskell, use it in addition to tcEqType to check that the visibility/specificity of expected forall-binders subsumes that of actual forall-binders.

  4. When tcEqType succeeds but tcSubVis fails, report an error message of the following form:

     • Visibility of forall-bound variables is not compatible
     Expected: forall a b. a -> b -> a
       Actual: forall {a} {b}. a -> b -> a

And that is exactly what I did in MR !9594 “Visibility subsumption”. It works, but I’m not sure if I implemented it in the best way possible, so I expect that it’ll take a few rounds of review before it’s done.

Let me know if you have any questions.

This work is funded by Serokell :purple_heart:

15 Likes
#2

If I understand correctly how it works, would this allow me to define “mandatory” type applications? For example something like

betterSymbolVal :: forall n . KnownSymbol n -> String

to be used like

demotedFoo :: String
demotedFoo = betterSymbolVal "foo" -- foo is a Symbol here

Some APIs of mine require type applications to work, and right now I have to put a big reminder about it in the docs, which is not ideal.

#3

KnownSymbol is a type class and the arrow needs to be next to the forall’d variable so it would be:

betterSymbolVal :: forall n -> KnownSymbol n => String

If my understanding is correct.

Also I don’t know if that application is going to work, because it will assume the string is a term. You might need to write:

demotedFoo = betterSymbolVal (type "foo")

All the details are in the proposal. Actually, example 4 in that proposal is much like your example:

-- Definition:
symbolValVis :: forall s -> KnownSymbol s => String
symbolValVis (type s) = symbolVal (Proxy :: Proxy s)

-- Usage
str = symbolValVis (type "Hello, World")

However, I think @int-index might just mean visible quantification in types of types, as it is not yet implemented on for types of terms.

1 Like
#4

Yes it will, just not right away: part 1 of the proposal requires the type specifier, but part 2 relaxes this restriction.

2 Likes
#5

Ah, I see. Scrolling further reveals example 4 in part II:

-- Definition:
symbolValVis :: forall s -> KnownSymbol s => String
symbolValVis s = symbolVal (Proxy :: Proxy s)

-- Usage
str = symbolValVis "Hello, World"
2 Likes