# More issues with `Coercible` solver

This page is to discuss further issues with the `Coercible` solver, and how to fix them. This is all spurred on by comment:9:ticket:10079, and affected by the implementation of the plan in comment:14:ticket:7788. The work-in-progress can be viewed at Phab:D653, or at my repo, branch `wip/rae`.

See examples at bottom of page.

## The Problem

Suppose we have `newtype N a = MkN rhs` and `[W] N t1 ~R N t2`, where `N` is a newtype whose constructor is in scope. We have two ways of proceeding: (1) either decompose to `[W] t1 ~r t2`, where the `r` is determined by the role on `N`'s parameter; or (2) unwrap `N` to expose its representation, simplifying to `[W] rhs[a |-> t1] ~R rhs[a |-> t2]`.

Approach (1) is always good except in the presence of a role annotation. By the correctness of role inference, `t1 ~r t2 <=> rhs[a |-> t1] ~R rhs[a |-> t2]`, assuming the role `r` is simply inferred from the structure of `rhs`. If `N` sports a role annotation, that assumption is bogus, and the arrow only points left. Thus, it's possible that decomposing gets us stuck, whereas unwrapping can yield an answer.

Approach (2) is always good unless the newtype is recursive. For a recursive newtype, approach (2) can trap us in an infinite loop.

Currently, we don't track whether or not a type has a role annotation, but we could. (We'd want to be careful not to treat a documentation-only role annotation as different from no role annotation, though.) Thus, if a type either has no role annotation or is non-recursive, we have a nice, complete algorithm. But, what on earth to do with recursive, role-annotated types?

### Why this is important

I (Richard E.) don't really know why recursive newtypes are all that important. But, role-annotated types are. It's easily conceivable that a library author wants a newtype whose constructor is held abstract. That author puts a role annotation on, preventing users from violating some key principle. But, the author also wants to coerce among different types freely in her own code. Thus, the solver needs, sometimes, to unwrap and not decompose. Indeed, this ability to coerce within a library but prevent coercions outside the library is a requested feature of the whole `Coercible` mechanism, and is advertised.

## Solutions

Simon and I agree that recursive newtypes aren't all that important, except in one case: when we have `newtype N a = ty`, we must be able to prove `N x ~R ty[a |-> x]`, even in the recursive case. Happily, this is captured by an eager reflexivity check, done after unwrapping. So, that's the plan going forward.

One very dissatisfying solution is to track role annotations and recursivity and then decide between decomposition and unwrapping based on these flags. For a role-annotated, recursive newtype, we just do our best, for some definition of best.

### How 7.10 works

There is a stop-gap solution in 7.10: see Note [Eager reflexivity check] in TcCanonical. Basically, the implementation prefers unwrapping, but checks for reflexivity before looping. This catches most, but not all cases. And it's a bit unprincipled. It will miss the following

```newtype B a = MkB [B a]

foo :: B Int -> B Bool
foo = coerce
```

## Examples

This is a collection of examples to think about when solving for `Coercible`. Some, but not all, of these are in the regression suite. They probably all should be.

`typecheck/should_compile/T9117`:

```newtype Phant a = MkPhant Char
type role Phant representational

ex1 :: Phant Bool
ex1 = coerce (MkPhant 'x' :: Phant Int)
```

Make sure that we unwrap when the constructor is in scope. Not recursive.

`typecheck/should_compile/T9117_2`:

```newtype Foo a = Foo (Foo a)
newtype Age = MkAge Int

ex1 :: (Foo Age) -> (Foo Int)
ex1 = coerce
```

Make sure that we don't unwrap when doing so would lead to an infinite loop. This example is rather perverse, so it might be reasonable to fail here.

`typecheck/should_compile/T9117_3`:

```eta :: Coercible f g => Coercion (f a) (g a)
eta = Coercion
```

Eta-expansion.

`typecheck/should_compile/T9117_4`:

```newtype Bar a = Bar (Either a (Bar a))
newtype Age = MkAge Int

x :: Bar Age
x = coerce (Bar (Left (5 :: Int)))
```

Like `T9117_2`, but not quite as perverse. This recursive newtype is at least inhabited.

`typecheck/should_fail/TcCoercibleFail`:

These should all fail:

```import Data.Ord (Down)

newtype Age = Age Int deriving Show

one :: Int
one = 1

type role Map nominal _
data Map a b = Map a b deriving Show

foo1 = coerce \$ one :: ()   -- utterly bogus

foo2 :: forall m. Monad m => m Age
foo2 = coerce \$ (return one :: m Int)   -- don't know the role of m

foo3 = coerce \$ Map one () :: Map Age ()   -- make sure we respect the role annotation

foo4 = coerce \$ one :: Down Int    -- make sure we respect not-imported constructor

newtype Void = Void Void
foo5 = coerce :: Void -> ()   -- utterly bogus, but shouldn't loop

foo5' = coerce :: (VoidBad ()) -> ()   -- ditto

-- This shoul fail with a context stack overflow
newtype Fix f = Fix (f (Fix f))
foo6 = coerce :: Fix (Either Int) -> Fix (Either Age)   -- stack overflow
foo7 = coerce :: Fix (Either Int) -> ()                 -- stack overflow / bogus
```

`typecheck/should_fail/TcCoercibleFail3`:

```data T f = T (f Int)

newtype NT1 a = NT1 (a -> Int)
newtype NT2 a = NT2 (a -> Int)

foo :: T NT1 -> T NT2
foo = coerce    -- should fail with stack overflow
```

This is a proper stack overflow. `NT1 Int` and `NT2 Int` are representationally equal in the limit. GHC is correct to keep unwrapping looking for this limit!

```foo :: f a -> f a
foo = coerce
```

Even though `AppTy`s can't be decomposed, we still must make sure that `Coercible` is reflexive!

```newtype X = MkX (Int -> X)

foo :: X -> X
foo = coerce
```

This could easily fall into an infinite loop, but we want this to succeed. Contrast with the `NT1`/`NT2` case a few examples up.

```newtype X a = MkX Char
type role X nominal

foo :: X Int -> X Bool
foo = coerce
```

This can succeed only by unwrapping, not by decomposition.

```newtype Age = MkAge Int
newtype Y a = MkY a
type role Y nominal

foo :: Y Age -> T Int
foo = coerce
```

Again, can succeed only by unwrapping, but has nothing to do with phantoms.

```newtype Z a = MkZ ()
type role Z representational

foo :: Z Int -> Z Bool
foo = coerce
```

Again only by unwrapping, but no nominal arguments.

```newtype N a = MkN [N a]
newtype Age = MkAge Int

foo :: N Age -> N Int
foo = coerce
```

Can succeed only by decomposition, because otherwise we loop.

```newtype App f a = MkApp (f a)

foo :: f a -> App f a
foo = coerce
```

Need to flatten/zonk before failing when we see an `AppTy`.

```newtype Q a = MkQ [Q a]

foo :: Q Bool -> Q Int
foo = coerce
```

Solvable by decomposition only. (`a` is phantom!)

```foo :: Coercible a b => b -> a
foo = coerce
```

Symmetry.

```foo :: (Coercible a b, Coercible b c) => a -> c
foo = coerce
```

Transitivity.

```foo :: (Coercible (a b) (c d), Coercible (c d) (e f)) => a b -> e f
foo = coerce
```

This should work, but this would require a lot more engineering. The problem is that `AppTy`s can't be decomposed, so it's hard to make the constraints canonical and then usable in substitution.

```newtype N1 a = MkN1 a
newtype N2 a = MkN2 (N1 a)

foo :: N1 a -> N2 a
foo = coerce
```

Here, we won't decompose, because the heads differ. Even though this is similar to a case where we do decompose. Simon says that this means we should prefer unwrapping. I agree.