TH eta-reduces away explicit foralls in data family instances (#15845) · Issues · Glasgow Haskell Compiler / GHC

TH eta-reduces away explicit foralls in data family instances

Consider the following code:

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Language.Haskell.TH

data family F1 a b
data instance F1 [a] b = MkF1

data family F2 a
data instance F2 a = MkF2

$(do i1 <- reify ''F1
     i2 <- reify ''F2
     runIO $ mapM_ (putStrLn . pprint) [i1, i2]
     pure [])

$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.7.20181101: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
data family Bug.F1 (a_0 :: *) (b_1 :: *) :: *
data instance forall (a_2 :: *). Bug.F1 ([a_2]) b_3 = Bug.MkF1
data family Bug.F2 (a_0 :: *) :: *
data instance Bug.F2 a_1 = Bug.MkF2

The output here is quite baffling:

In the F1 instance, we have an explicit forall which quantifies a_2 but not b_3!
In the F2 instance, there isn't an explicit forall at all despite the fact that there ought to be one, since there is a type variable a_1 in this instance.

The culprit in both of the bullet points above is the fact that GHC eta-reduces its internal representation of data family instance axioms. This is the same thing which caused #9692 (closed) and #14179 (closed), in fact. Luckily, the same fix for those tickets will also work here.

Patch incoming.

Trac metadata

Trac field	Value
Version	8.7
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Template Haskell
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

Consider the following code:

```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Language.Haskell.TH

data family F1 a b
data instance F1 [a] b = MkF1

data family F2 a
data instance F2 a = MkF2

$(do i1 <- reify ''F1
     i2 <- reify ''F2
     runIO $ mapM_ (putStrLn . pprint) [i1, i2]
     pure [])
```

```
$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.7.20181101: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
data family Bug.F1 (a_0 :: *) (b_1 :: *) :: *
data instance forall (a_2 :: *). Bug.F1 ([a_2]) b_3 = Bug.MkF1
data family Bug.F2 (a_0 :: *) :: *
data instance Bug.F2 a_1 = Bug.MkF2
```

The output here is quite baffling:

- In the `F1` instance, we have an explicit `forall` which quantifies `a_2` but not `b_3`!
- In the `F2` instance, there isn't an explicit `forall` at all despite the fact that there ought to be one, since there is a type variable `a_1` in this instance.

The culprit in both of the bullet points above is the fact that GHC eta-reduces its internal representation of data family instance axioms. This is the same thing which caused #9692 and #14179, in fact. Luckily, the same fix for those tickets will also work here.

Patch incoming.

<details><summary>Trac metadata</summary>

| Trac field             | Value            |
| ---------------------- | ---------------- |
| Version                | 8.7              |
| Type                   | Bug              |
| TypeOfFailure          | OtherFailure     |
| Priority               | normal           |
| Resolution             | Unresolved       |
| Component              | Template Haskell |
| Test case              |                  |
| Differential revisions |                  |
| BlockedBy              |                  |
| Related                |                  |
| Blocking               |                  |
| CC                     |                  |
| Operating system       |                  |
| Architecture           |                  |

</details>