# GHC+DH Weekly Update #2, 2022-12-21
**URL:** https://discourse.haskell.org/t/ghc-dh-weekly-update-2-2022-12-21/5473
**Category:** Uncategorized
**Created:** [December 21, 2022, 1:04pm UTC](https://discourse.haskell.org/t/ghc-dh-weekly-update-2-2022-12-21/5473 "2022-12-21T13:04:54Z")
**Posts on this page:** 5
**Page:** 1
### Author:  [@int-index](https://discourse.haskell.org/u/int-index)
#### Post date: [December 21, 2022, 1:04pm UTC](https://discourse.haskell.org/t/ghc-dh-weekly-update-2-2022-12-21/5473/1 "2022-12-21T13:04:54Z")
Hi all, here’s another update on the implementation of dependent types in GHC.
This time I worked on solving an issue with visibility of type variables. In GHC, a forall-bound variable may have one of the three visibilities:
- required, written `forall a ->`
- specified, written `forall a.`
- inferred, written `forall {a}.`
This distinction is important in surface Haskell, but it does not make any difference in Core. So in an ideal world, we would be careful to track it in the type checker and discard it afterwards. At the moment, however, GHC does neither. The current design is to play fast and loose with the specified vs inferred distinction, but be strict about required vs non-required variables. This results in the worst of both worlds:
1. in Core, we can not use lambdas to bind required variables
2. in Haskell, we can accidentally write programs that rely on the implementation details of GHC’s kind inference engine
The first issue is what drew my attention to this. In fact, it is a blocker for [MR !9257](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9257), so it needs to be addressed to make progress on dependent types. The second issue, however, also deserves some attention, and I opened [#22648](https://gitlab.haskell.org/ghc/ghc/-/issues/22648) to track it.
Fortunately, we can kill two birds with one stone if we implement _visibility subsumption_. The idea is as follows:
1. Ignore visibility of `forall`-bound variables in `eqType` and `tcEqType` completely.
2. Define a subsumption relation between the expected and actual `ForAllTyFlag`:
3. Define a new check `tcSubVis`:
4. When `tcEqType` succeeds but `tcSubVis` fails, report an error message of the following form:
And that is exactly what I did in [MR !9594](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9594) **“Visibility subsumption”**. It works, but I’m not sure if I implemented it in the best way possible, so I expect that it’ll take a few rounds of review before it’s done.
Let me know if you have any questions.
* * *
This work is funded by [Serokell](https://serokell.io/) 💜
---
### Author:  [@danidiaz](https://discourse.haskell.org/u/danidiaz)
#### Post date: [December 21, 2022, 7:00pm UTC](https://discourse.haskell.org/t/ghc-dh-weekly-update-2-2022-12-21/5473/2 "2022-12-21T19:00:27Z")
> [@int-index](#):
>
> required, written `forall a ->`
If I understand correctly how it works, would this allow me to define “mandatory” type applications? For example something like
```haskell
betterSymbolVal :: forall n . KnownSymbol n -> String
```
to be used like
```haskell
demotedFoo :: String
demotedFoo = betterSymbolVal "foo" -- foo is a Symbol here
```
Some APIs of mine require type applications to work, and right now I have to put a big reminder about it in the docs, which is not ideal.
---
### Author:  [@jaror](https://discourse.haskell.org/u/jaror)
#### Post date: [December 21, 2022, 7:56pm UTC](https://discourse.haskell.org/t/ghc-dh-weekly-update-2-2022-12-21/5473/3 "2022-12-21T19:56:30Z")
KnownSymbol is a type class and the arrow needs to be next to the forall’d variable so it would be:
```haskell
betterSymbolVal :: forall n -> KnownSymbol n => String
```
If my understanding is correct.
Also I don’t know if that application is going to work, because it will assume the string is a term. You might need to write:
```haskell
demotedFoo = betterSymbolVal (type "foo")
```
All the details are in [the proposal](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst). Actually, example 4 in that proposal is much like your example:
```haskell
-- Definition:
symbolValVis :: forall s -> KnownSymbol s => String
symbolValVis (type s) = symbolVal (Proxy :: Proxy s)
-- Usage
str = symbolValVis (type "Hello, World")
```
However, I think @int-index might just mean visible quantification in types of types, as it is not yet implemented on for types of terms.
---
### Author:  [@int-index](https://discourse.haskell.org/u/int-index)
#### Post date: [December 21, 2022, 7:59pm UTC](https://discourse.haskell.org/t/ghc-dh-weekly-update-2-2022-12-21/5473/4 "2022-12-21T19:59:32Z")
> [@jaror](#):
>
> I don’t know if that application is going to work, because it will assume the string is a term.
Yes it will, just not right away: part 1 of the proposal requires the `type` specifier, but part 2 relaxes this restriction.
---
### Author:  [@jaror](https://discourse.haskell.org/u/jaror)
#### Post date: [December 21, 2022, 8:05pm UTC](https://discourse.haskell.org/t/ghc-dh-weekly-update-2-2022-12-21/5473/5 "2022-12-21T20:05:36Z")
Ah, I see. Scrolling further reveals example 4 in part II:
```haskell
-- Definition:
symbolValVis :: forall s -> KnownSymbol s => String
symbolValVis s = symbolVal (Proxy :: Proxy s)
-- Usage
str = symbolValVis "Hello, World"
```