This module provides functionality for recognising whether a type is a TyConApp while taking into account Given nominal equalities.

In particular, this allows dealing with flattening variables on older GHC versions (9.0 and below). For example, instead of [W] m + n ~ n + m, older GHCs might produce [G] u ~ m + n, [G] v ~ n + m, [W] u ~ v. In this case, one needs to use the Givens to recognise that u ~ v can be solved using the laws of natural number arithmetic.

Usage:

• Use mkTyConSubst to create a TyConSubst from Givens.
• Use splitTyConApp_upTo to compute whether a type is a TyConApp, taking into account Given constraints (in the form of the TyConSubst).

Notes:

• splitTyConApp_upTo will also look through type synonyms,
• splitTyConApp_upTo only takes into account nominal equalities. Please open a ticket if you have a need for rewriting modulo representational equalities.