I support. Simon On Tue, 29 Aug 2023 at 07:48, Vladislav 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@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Looks like an overall improvement to me. I’m in support. On Tue, 29 Aug 2023 at 2:48 PM, Vladislav 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@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee