## ScopedTypeVariables could allow more programs

Consider

```
data P a = P
data T1 a where
MkT1 :: forall a. P a -> T1 a
MkT2 :: forall a. P a -> T1 (a,a)
MkT3 :: forall a b. b ~ Int => P a -> P b -> T1 a
MkT4 :: forall a b. P a -> P b -> T1 a
MkT5 :: forall a b c. b ~ c => P a -> P b -> P c -> T1 a
```

I can write this function

```
foo :: T1 (Int, Int) -> ()
foo (MkT1 (P::P (Int,Int))) = ()
foo (MkT2 (P::P x)) = (() :: x ~ Int => ())
foo (MkT3 P (P::P Int)) = ()
foo (MkT4 P (P::P b)) = ()
foo (MkT5 P (P::P b) (P::P b)) = ()
```

but this these two equations fail

```
foo (MkT1 (P::P (Int,x))) = (() :: x ~ Int => ())
foo (MkT1 (P::P x)) = (() :: x ~ (Int,Int) => ())
```

I am especially surprised by the second one, given that the very similar equation with `MkT2`

works.

## Trac metadata

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

Version | 8.4.1 |

Type | FeatureRequest |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information