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 forallbound 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 nonrequired variables. This results in the worst of both worlds:
 in Core, we can not use lambdas to bind required variables
 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:

Ignore visibility of
forall
bound variables ineqType
andtcEqType
completely. 
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

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 expectedforall
binders subsumes that of actualforall
binders.

When
tcEqType
succeeds buttcSubVis
fails, report an error message of the following form:• Visibility of forallbound 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