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”.)