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

[Vladislav]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20230829/5ac72265/attachment.html>