v2

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

newtype VoidBad a = VoidBad (VoidBad (a,a))
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 AppTys 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 AppTys 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.

v2

More issues with Coercible solver