## Trivial partial type signature kills type inference in the presence of GADTs

Suppose we have

```
data G a where
G1 :: G Char
G2 :: G Bool
```

If I now write

```
foo x = case x of
G1 -> 'z'
G2 -> True
```

I rightly get an error around untouchable variables.

If I add the type signature

`foo :: G a -> a`

all is well again. So far, so good.

Now, I write

```
foo :: forall a. G a -> a
foo x = ((case x of
G1 -> 'z'
G2 -> True) :: _)
```

and I get those untouchable errors again. Untouchable-variable errors usually arise when there are multiple possible answers to the type inference problem. Yet, that isn't the case here: `_`

must stand for `a`

.

Solution: mumble mumble bidirectional type inference mumble mumble.

Part of the problem comes from Note [Partial expression signatures] in TcExpr, which states

```
here is a guiding principile
e :: ty
should behave like
let x :: ty
x = e
in x
```

Indeed, if we behave like that, the untouchable-variable errors are to be expected. But I also think that it would be a nice principle to say that `:: _`

is always a no-op.

This is not an idle nice-to-have: if we fix this, `singletons`

will continue to work with GHC. Right now, it doesn't: https://github.com/goldfirere/singletons/issues/357

## Trac metadata

Trac field | Value |
---|---|

Version | 8.6.3 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |