Like tcLookupDataFamInst_maybe, but returns the arguments back if there is no data family to unwrap. Returns a Representational coercion

Converts a data family type (eg F [a]) to its representation type (eg FList a) and returns a coercion between the two: co :: F [a] ~R FList a.

tcUnwrapNewtype_maybe gets rid of one layer of top-level newtypes

It is only used by the type inference engine (specifically, when solving representational equality), and hence it is careful to unwrap only if the relevant data constructor is in scope. That's why it gets a GlobalRdrEnv argument.

It is capable of unwrapping a newtype instance. E.g data D a newtype instance D Int = MkD Bool Then `tcUnwrapNewtype_maybe (D Int)` will unwrap to give the Bool inside. However, it is careful not to unwrap data/newtype instances if it can't unwrap the newtype inside it; that might in the example if MkD was not in scope. Such care is necessary for proper error messages.

It does not look through type families. It does not normalise arguments to the tycon.

If the result is Right (gre, co, rep_ty), then:

• co : ty ~R rep_ty
• gre is the GRE for the data constructor that had to be in scope

If the result is Left explns, then we failed to unwrap, and explns stores any information we would like to report to the user about why we failed to unwrap (e.g. failed to unwrap because the newtype constructor was out of scope). See Note [CtExplanations] in GHC.Tc.Types.CtLoc. This might be empty (e.g. if the type is not a newtype at all).

Report a list of injectivity errors together with their source locations. Looks only at one equation; does not look for conflicts *among* equations.

Report error message for a pair of equations violating an injectivity annotation. No error message if there are no branches.