More issues with
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
See examples at bottom of page.
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
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.
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
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.
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.
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.
eta :: Coercible f g => Coercion (f a) (g a) eta = Coercion
newtype Bar a = Bar (Either a (Bar a)) newtype Age = MkAge Int x :: Bar Age x = coerce (Bar (Left (5 :: Int)))
T9117_2, but not quite as perverse. This recursive newtype is at least inhabited.
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
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
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
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
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
foo :: (Coercible a b, Coercible b c) => a -> c foo = coerce
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.