GHC+DH Weekly Update #5, 2023-01-25

#1

Hi all, this is the fifth weekly update on the implementation of dependent types in GHC.

First and foremost, I’m happy to share that Serokell allocated one more software engineer to work on GHC. Andrey is going to start with GHC Proposal #475 “Non-punning list and tuple syntax” (ticket #21294). He has also kindly agreed to post his weekly reports alongside mine. Thank you Andrey!

As for me, I continued to work on MR !9480 “Invisible binders in type declarations” and fixed the outstanding TODOs. I improved the error messages, wrote a User’s Guide section on @k-binders, implemented TH reification of invisible binders, and summarized the changes in a commit message. At this point, I felt that the patch was good enough for review, so I removed the “Draft” label.

Ryan helpfully reviewed the patch and identified a set of potential improvements. He convinced me to remove reification of invisible binders to avoid a silent breaking change. Consider the following declaration:

data P @k (a :: k) = MkP

Should reify return the @k binder or not? You can find the discussion at #22828 “Reification of invisible type variable binders”.

Ryan also came up with additional examples for the test suite:

-- type U :: forall {k} (a :: k). Type
type U @a = Int

-- type Z :: forall k -> forall (a :: k). Type
type Z k @(a :: k) = Proxy a

--  Conflicting definitions for ‘k’
--  Bound at: T22560_fail_c.hs:3:11
--            T22560_fail_c.hs:3:14
data Dup @k @k (a :: k)

Based on his feedback, I also refactored rnLHsTyVarBndrVisFlag and mkExplicitTyConBinder.

Unless something unexpected comes up, I think this task is fairly close to completion.

MR !9594 “Visibility subsumption”, on the other hand, proved to be more of a challenge than I hoped it would be. It’s a swamp of tricky design questions! Simon and I tried to move checkSubVis out of the unifier and place it in tcApp. But then I spotted a failing test, which I minimized to:

type V :: forall k -> k -> Type
data V k (a :: k) = MkV

f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> ()
f _ = ()

bad :: ()
bad = f MkV

Here we end up unifying hk with V, which have the following kinds:

  • hk :: forall j. j -> Type
  • V :: forall k -> k -> Type

Unfortunately, checkSubVis fails to detect that we unified visible and invisible foralls because one of them is hidden in the kind of a unification variable. Interestingly, we can detect this if visible type application is used:

bad :: ()
bad = f @V MkV

This modified example correctly produces the following error message:

Example.hs:14:10: error: [GHC-25115]
    • Visibility of forall-bound variables is not compatible
        Expected: forall j. j -> *
          Actual: forall k -> k -> *
    • In the type ‘V’
      In the expression: f @V MkV
      In an equation for ‘bad’: bad = f @V MkV

Well, at least we’ve got that going for us. More thought is required to figure out what to do when the visible type application is absent.

Let me know if you have any questions.

This work is funded by Serokell :purple_heart:

9 Likes
Status of dependent types?
#2

Hi everyone, I am a new member of the Serokell GHC team. As I didn’t have experience with GHC before, I thought it would be interesting for others in the Haskell community to hear about the work that a junior developer can do in the GHC codebase. Here’s my first report.

This week, I focused on two different issues. The first of them is part of the Non-punning list and tuple syntax proposal. This proposal allows the user to write pun-free code, making it easier to mix type-level and term-level names, which is going to happen often in dependently-typed code.

When I started working on implementing this proposal, parts of it were already implemented in:

  • Commit 02279a9c renamed the [] type constructor to List
  • Commit adf3302c renamed the Solo data constructor to MkSolo

I identified a minor issue with pretty-printing of MkSolo. The ppr_mono_ty function in GHC.Hs.Type contains the following comment:

-- Special-case unary boxed tuples so that they are pretty-printed as
-- `'Solo x`, not `'(x)`

We want the code pretty-printed by GHC to be valid, but 'Solo is no longer a valid promoted data constructor. After looking at the code, I found out that this is not just an outdated comment, but an omission in the aforementioned commit.

The next step was to find the code that would trigger this code path, so I would be able to test the fix that I had in mind. The solution is simple: remove the special case for unary tuples and run the entire test suite. I immediately found a bunch of failing tests related to TH. I extracted the code produced by TH and constructed the following code snippet:

{-# LANGUAGE DataKinds #-}
module T where
import Data.Proxy
import Data.Tuple

p :: Proxy ('MkSolo Int)
p = Proxy :: Proxy Int

I also created a new issue #22785 with it. Turns out that my code triggers a different code path from the first one, which I didn’t know at the time. Actually GHC has three ways to pretty-print a type:

  • The first one is in the GHC.Hs.* modules.
  • The second one is in the GHC.Iface.* modules and it is related to pretty printing of types from interface files.
  • The third one is the pprint function from the template-haskell library. Interestingly enough, dumping the TH splices triggers pretty-printing from GHC.Hs, not from template-haskell.

Then I started reading code to find how the output strings "Solo" and "MkSolo" were constructed and found that all relevant logic is in the GHC.Buitin.Types module, where the mkBoxedTupleStr function is defined thus:

mkBoxedTupleStr :: NameSpace -> Arity -> String
mkBoxedTupleStr _ 0  = "()"
mkBoxedTupleStr ns 1 | isDataConNameSpace ns = "MkSolo"  
mkBoxedTupleStr _ 1 = "Solo"                        	 
mkBoxedTupleStr _ ar = '(' : commas ar ++ ")"

And two wrappers: tupleDataConName (produces "MkSolo") and tupleTyConName (produces "Solo"), so my task was to find all usages of tupleTyConName and check if I should add a case that will call tupleDataConName depending on the context.

There were only two modules that I had to change: GHC.Hs.Type and GHC.Iface.Type. Here is an MR !9733 which is already merged. Perhaps we need to backport this patch to the GHC 9.6.

The second issue was about error messages. There are a bunch of refactorings in GHC the main goal of which is to improve GHC API. One of them is about moving from strings as errors to values as errors, and you can read more about it in the issue #19905. This task is important to the HLS team, and the main challenge is the vast amount of errors that need to be converted. If you would like to contribute to GHC, I suggest starting with this issue.

I picked a sub-issue from the main one. It is described in #20115. The main idea is that I should convert the usages of TcRnUnknownMessage to the new constructors of TcRnMessage. TcRnMessage is a huge sum type (200 constructors at the moment).

If you want to add new error constructors, you need to handle them in the following functions in the GHC.Tc.Errors.Ppr module:

  • diagnosticMessage that produces a human-readable error message
  • diagnosticReason that classifies messages into errors and warnings, unconditional and guarded behind a flag
  • diagnosticHints that suggests to enable language extensions or to fix the error in other ways

Then you have to add a new diagnostic code in the GHC.Types.Error.Codes module.

Diagnostic codes are the new initiative of the Haskell Foundation. It is part of the 024 Error Messages proposal announced in discourse here. You can look up and read about these codes at https://errors.haskell.org/. Great work, HF!

So, I took the GHC.Rename.Bind module and converted all usages of mkTcRnUnknownMessage into 11 new constructors of TcRnMessage.

The second step was to describe new errors, find tests that cover them, and provide simple examples when possible. It is possible to shorten this part significantly if you always read the documentation: hadrian has a suitable option to automatically update test outputs: -a/--test-accept. Don’t forget to check the updated files into git!

Now the MR !9792 with those changes is under review.

That’s all for today! I would be glad to hear what you think and if you have any advice on GHC development.

This work is funded by Serokell :purple_heart:

10 Likes
#3

Thanks for helping complete the migration to an error datatype! It really does enable lots of great use cases.

3 Likes
#4

Request for the future of these posts: can you type the full phrase “dependent haskell” in the title? Because discourse does not allow to search on the keyword “dh” as it is too short.

#5

For what it is worth, “GHC+DH” is long enough, so that at least serves as a workaround. The discoverability is certainly lower, though.

Big fan of these posts!