Opened 4 months ago

Closed 2 months ago

Last modified 7 weeks ago

#15497 closed task (fixed)

Coercion Quantification

Reported by: ningning Owned by:
Priority: normal Milestone:
Component: Compiler Version:
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D5054
Wiki Page: https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2

Description

As described in https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2.

We would like to have coercion quantifications back in Haskell Core language.

This means in Core we can define types like

\/ (a: k1) . 
  \/ (co : k1 ~ k2)  -- an explicit quantification for the coercion
  -> (a |> co)       -- use the name for an explicit cast
  -> ...

Change History (12)

comment:1 Changed 3 months ago by simonpj

Differential Rev(s): Phab:D5054

comment:2 Changed 3 months ago by Richard Eisenberg <rae@…>

In ea5ade34/ghc:

Coercion Quantification

This patch corresponds to #15497.

According to https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2,
 we would like to have coercion quantifications back. This will
allow us to migrate (~#) to be homogeneous, instead of its current
heterogeneous definition. This patch is (lots of) plumbing only. There
should be no user-visible effects.

An overview of changes:

- Both `ForAllTy` and `ForAllCo` can quantify over coercion variables,
but only in *Core*. All relevant functions are updated accordingly.
- Small changes that should be irrelevant to the main task:
    1. removed dead code `mkTransAppCo` in Coercion
    2. removed out-dated Note Computing a coercion kind and
       roles in Coercion
    3. Added `Eq4` in Note Respecting definitional equality in
       TyCoRep, and updated `mkCastTy` accordingly.
    4. Various updates and corrections of notes and typos.
- Haddock submodule needs to be changed too.

Acknowledgments:
This work was completed mostly during Ningning Xie's Google Summer
of Code, sponsored by Google. It was advised by Richard Eisenberg,
supported by NSF grant 1704041.

Test Plan: ./validate

Reviewers: goldfire, simonpj, bgamari, hvr, erikd, simonmar

Subscribers: RyanGlScott, monoidal, rwbarton, carter

GHC Trac Issues: #15497

Differential Revision: https://phabricator.haskell.org/D5054

comment:3 Changed 3 months ago by ningning

Owner: set to ningning

comment:4 Changed 3 months ago by ningning

Resolution: fixed
Status: newclosed

comment:5 Changed 3 months ago by simonpj

Owner: ningning deleted
Resolution: fixed
Status: closednew

I came across Note [Emitting the residual implication in simplifyInfer] in TcSimplify. It says “We can't form types like (forall co. blah), so we can't generalise over the coercion variable, …”

But when you commit coercion quantification, we can quantify over coercions in types. So it is possible that this bit of cruft could be tidied up, with a significant simplification.

I'll re-open the ticket to keep this idea on the radar.

comment:6 Changed 3 months ago by simonpj

Keywords: TypeInType added

comment:7 Changed 2 months ago by ningning

I have looked through TcSimplify and 14584, but I am unsure I have understood fully the details. The logic seems delicate there. I know the motivation is

forall x[2].
   [W] co1: alpaha[1] ~ ty |> co2
   [W] co2: k1 ~ *

where we have the scope problem cause co2 could mention x and co1 depends on co2.

What's the goal after we have coercion quantifications comparing to the current strategy??

comment:8 Changed 2 months ago by goldfire

Resolution: fixed
Status: newclosed

comment:5 really seems to be asking for #15710. Closing this ticket in favor of that one.

comment:9 Changed 2 months ago by simonpj

On coercion quantification, I think it would be helpful to update DependentHaskell/Phase2

  • Under "Why homogeneous equality is good" explain how homogeneous equality can help the simplifier (in exprIsConApp_maybe).
  • On the same page, under "A small wrinkle: we need coercion quantification back", remove or rephrase the stuff about (~~); perhaps use the data type :~~: rather than the class (~~).
  • Promote "Another approach" for the class (~~) which appears lower down. It may be another approach but it is Our Plan for solving a Real Problem in introducing homogeneous equality at the moment, and as time goes on it is really helpful to know what The Plan is, with other approaches being discussed later.

TL;DR: make the page reflect our current thinking as directly as possible.

comment:10 Changed 2 months ago by simonpj

One other thing. As I said in our call today, it's striking how narrow are the use-cases for a coercion-quantified type:

  • We can't declare a function with type f :: (t1 ~# t2) => blah, because currently (t1 ~# t2) is not a constraint (see Trac #15648) and is never implicitly instantiated.
  • We can't infer a function with type f :: (t1 ~# t2) => blah. And if we did, it wouldn't be instantiated implicitly.

And so a fortiori we can't have coercion-quantified variants of such types.

So the only functions that can have these coercion-quantified types are the workers of data constructors. Am I right? If so, can we say so explicitly on the wiki page?

That seems like a lot of work for a narrow use-case! And yet, and yet... it's a very important case.

Note also that we cannot write an exactly-equivalent type signature with GADT-syntax, because we don't have source-syntax of t1 ~# t2, let alone for forall (co:t1~#t2). blah.

comment:11 Changed 2 months ago by goldfire

I've done these wiki updates. Thanks for the concrete suggestions.

comment:12 Changed 7 weeks ago by Ningning Xie <xnningxie@…>

In 3905c3c/ghc:

Update core-spec for Coercion Quantification

Summary:
Update details for `ForAllTy` and `ForAllCo` in core-spec, as they
can now quantify over coercion variables.

Test Plan: Please read core-spec.pdf

Reviewers: goldfire, simonpj, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, carter

GHC Trac Issues: #15497, #15589

Differential Revision: https://phabricator.haskell.org/D5247
Note: See TracTickets for help on using tickets.