[ghc-steering-committee] #607: Amend #281 (visible forall) and #378 (Design of DH) to clarify treatment of term variables in types (rec: accept)

[Arnaud Spiwack]

This seems highly uncontroversial to me. I'm happy to support the amendment.

On Tue, 29 Aug 2023 at 08:48, Vladislav <vlad.z.4096 at gmail.com> wrote:

> Dear Committee,
>
> Jakob Brünker has proposed #607, an amendment to proposals #281 (visible
> forall) and #378 (Design of DH).
> See the diff here:
> https://github.com/ghc-proposals/ghc-proposals/pull/607/files
>
> The amendment concerns type checking of term-level variables appearing in
> types, for example:
>
>   f :: forall (a :: Bool) -> ...   -- visible forall, `f` expects a
> type-level Bool
>   g :: Bool -> ...  -- ordinary arrow, `g` expects a term-level Bool
>   g x = f x
>
> What should happen to `x`, bound as a term variable but used as a type?
> #378 "Design for Dependent Types" already has an answer to this question:
> treat `x` as a skolem. But there are two problems
>
> 1. #378 does not explain this design decision in sufficient detail. This
> led Simon to question its inclusion: "Does it have any value, really? Why
> not just reject?"
> 2. #281 follows this design in one section, saying "treated as a fresh
> skolem constant"; and rejects it in another section, saying "any uses of
> terms in types are ill-typed". There is a contradiction.
>
> The amendment addresses both issues as follows:
>
> 1. A new example is added to #378, explaining how treating `x` as a skolem
> is useful, but only if `foreach` is available (a retained quantifier that
> allows dependent pattern matching)
> 2. Contradiction in #281 is resolved in favor of rejecting any uses of
> terms in types as ill-typed, saving this feature for a future proposal.
>
> I recommend to accept. Please share your thoughts either here or directly
> on GitHub.
>
> Vlad
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>


-- 
Arnaud Spiwack
Director, Research at https://moduscreate.com and https://tweag.io.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20230829/aeee6420/attachment.html>