Rejecting overlapping quantified constraints prevents this weird trick.

The rules for coercing a newtype require the constructor being in scope. I was experimenting with the following idiom, where the constructor is not exported, but a function that that would “locally”, in its argument, enable coerce to look through the newtype:

A.hs:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FlexibleContexts #-}
module A(A, unsafeWithA) where

import Data.Coerce

newtype A a = A [a]

unsafeWithA :: (
  ( forall a b. Coercible [a] b => Coercible (A a) b
  , forall a b. Coercible b [a] => Coercible b (A a)
  ) => x) -> x
unsafeWithA x = x

So the argument to unsafeWithA is type-checked with extra given constraints that should tell the type checker to look through A.

It works most, but not always: B.hs:

import A
import Data.Coerce

works1 :: A a -> [a]
works1 = unsafeWithA coerce

works2 :: (A a,[b]) -> ([a], A b)
works2 = unsafeWithA coerce

newtype Age = Age Int

works3 :: A Age -> [Int]
works3 = unsafeWithA coerce

works4 :: A Int -> [Age]
works4 = unsafeWithA coerce

does'ntWork :: A Int -> A Age
does'ntWork = unsafeWithA coerce

In the last case, the problem is that there are now two quantified constraints that GHC could apply, unrolling A first on the left or first on the right, so as documented in https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/quantified_constraints.html#overlap, it just doesn't do anything.

I am not requesting that the “Reject if in doubt” rule gets abandoned. This was just an experiment, and I am not sure this idiom is that useful. But I wanted to write it down somewhere, and I hope this is a reasonable place for it. If anything, maybe the feature request is that I’d like to able to write

unsafeWithA :: (C => x) -> x
unsafeWithA x = x

in A.hs so that in a use of unsafeWithA e, the e is type-checked as if A’s construct was in scope. (Maybe we could use a built-in constraints IsNewTypeAndConstructorIsInScope to get a handle on this “capability”.)