GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2024-01-23T14:31:17Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/24330hpc complains that record field referencing an existential is never executed2024-01-23T14:31:17ZShea Levyshea@shealevy.comhpc complains that record field referencing an existential is never executed## Summary
```haskell
{-# LANGUAGE ExistentialQuantification #-}
module Main where
data Any = forall a. Any { any :: a }
main :: IO ()
main = do
let x = Any 'c'
case x of
Any _ -> pure ()
```
![image](/uploads/f561b311655ef76...## Summary
```haskell
{-# LANGUAGE ExistentialQuantification #-}
module Main where
data Any = forall a. Any { any :: a }
main :: IO ()
main = do
let x = Any 'c'
case x of
Any _ -> pure ()
```
![image](/uploads/f561b311655ef76e403e6a69bfcce000/image.png)
## Steps to reproduce
`ghc -fhpc Test.hs && ./Test && hpc report Test`
## Expected behavior
`any` is not marked up as `never executed`, as there is no way to call it
## Environment
* GHC version used: 9.2.4, 9.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/20865The GADTs extension implies ExistentialQuantification2022-01-03T14:41:36ZMarioThe GADTs extension implies ExistentialQuantification## Summary
According to the User's Guide section on `GADTs`, the extension implies only `MonoLocalBinds` and `GADTSyntax`.
http://downloads.haskell.org/~ghc/latest/docs/html/users_guide/exts/gadt.html
However the following short progr...## Summary
According to the User's Guide section on `GADTs`, the extension implies only `MonoLocalBinds` and `GADTSyntax`.
http://downloads.haskell.org/~ghc/latest/docs/html/users_guide/exts/gadt.html
However the following short program compiles so it seems that `ExistentialQuantification` is also implied by `GADTs`:
```
{-# LANGUAGE GADTs #-}
module T16344 where
data T3 a = forall b. MkT3 (T3 b)
```
## Proposed improvements or changes
I'm assuming this is an oversight in User's Guide, rather than a GHC bug. IMO it makes sense to require `ExistentialQuantification`: it's definitely allowed in GADT-style declarations, so why not in regular syntax as well?
In this case, the fix is trivial: just add the `ExistentialQuantification` to the two extensions already implied by `GADTs`.
## Environment
* GHC version used (if appropriate): 9.2.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/20337Projecting existential variables2021-09-07T14:24:46ZJohn EricsonProjecting existential variableshttps://richarde.dev/papers/2021/exists/exists.pdf shows how we can project existential variables, using the expressions themselves to "non-generatively" introduce special skolems, rather than be confined to pattern matching and getting ...https://richarde.dev/papers/2021/exists/exists.pdf shows how we can project existential variables, using the expressions themselves to "non-generatively" introduce special skolems, rather than be confined to pattern matching and getting fresh skolems confined to scopes. These "applicative skolems" (to continue to borrow the ML functor terminology), are a nice thing to have with or without `exists a. ...` new "structural" existential types.
With lots of other hypothetical syntax:
```haskell
data Foo where
MkFoo :: forall a. Show a => a :: Foo
_1 :: Foo -> Type -- but indicate non-relevant somehow?
_2 :: forall (a :: Foo) -> Dict (Show (fst a))
_3 :: forall (a :: Foo) -> fst a
foo :: Foo -> String
foo f = case _2 a of
Dict -> show x
where
type T = _1 a
x :: T = _3 a
```
`_2` requires `case`, but that is only because of `Dict`. We could imagine explicit dictionary arguments or something instead, but that is separate.
The paper also goes into term-level constraints, which seems good for Dependent Haskell in general, but I suppose that should also have a separate issue.
CC @raeResearch neededhttps://gitlab.haskell.org/ghc/ghc/-/issues/16693Order of declarations affects which programs are accepted (type families and ...2020-01-23T19:39:43ZIavor S. DiatchkiOrder of declarations affects which programs are accepted (type families and existentials)Consider the following example:
```haskell
{-# LANGUAGE ExistentialQuantification, TypeFamilies #-}
module Bug where
type family G n
type instance G a = F
data T = forall w. T (G w)
type family F where F = ()
-- type family G n
```
GH...Consider the following example:
```haskell
{-# LANGUAGE ExistentialQuantification, TypeFamilies #-}
module Bug where
type family G n
type instance G a = F
data T = forall w. T (G w)
type family F where F = ()
-- type family G n
```
GHC rejects this program, when checking if `T` is ambiguous. However, if I move the declaration of `G` to the end of the file (the declaration that is commented out), then GHC accepts the program.
I would guess that, somehow, it matters in what order things are processed---if `G` is evaluated fully first, it can resolve to `()` and there is no ambiguity. However, if `G` is not evaluated, then there appears to be an ambiguity as `w` occurs under a type family.Vladislav ZavialovVladislav Zavialov