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

[Adam Gundry]

Agreed, this looks sensible to me.

Adam


On 29/08/2023 23:57, Richard Eisenberg wrote:
> Yes, in support. Thanks for the nice summary.
> 
> Richard
> 
>> On Aug 29, 2023, at 4:40 AM, Moritz Angermann 
>> <moritz.angermann at gmail.com <mailto:moritz.angermann at gmail.com>> wrote:
>>
>> Looks like an overall improvement to me. I’m in support.
>>
>> On Tue, 29 Aug 2023 at 2:48 PM, Vladislav <vlad.z.4096 at gmail.com 
>> <mailto: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
>>     <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

-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, https://www.well-typed.com/

Registered in England & Wales, OC335890
27 Old Gloucester Street, London WC1N 3AX, England