Unsoundness when combining ValueOf and instance chains

[zyla]

It seems that in some cases the compiler may choose different instances from an instance chain in different places. Since ValueOf coercions depend on the uniqueness of instances, this can lead to unsoundness. Here's an example:

module InstanceChains where

import Prelude

import Data.Array as Array
import Debug (traceM)
import Effect (Effect)
import Type.Eval (class Eval, TypeExpr)
import Type.Eval.ValueOf (ValueOf)
import Type.Eval.ValueOf as ValueOf

foreign import data F :: Type -> TypeExpr Type

instance Eval (F (Array a)) a
else instance Eval (F a) a

coerceFromF :: forall a. ValueOf (F a) -> a
coerceFromF = ValueOf.to

coerceToF :: forall a. a -> ValueOf (F (Array a))
coerceToF = ValueOf.from

shouldNotHappen :: forall a. a -> Array a
shouldNotHappen = coerceFromF <<< coerceToF

main :: Effect Unit
main = do
  let ostensiblyArray :: Array Int
      ostensiblyArray = shouldNotHappen 1
  traceM (Array.length ostensiblyArray)

This compiles and prints undefined.

The problematic instance resolution seems to happen in coerceFromF, where the second instance is always chosen despite the type constructor not being known to be different from Array.

I don't know enough about instance chains to tell if this is the expected behavior; it's not intuitive to me, but maybe that's how instance chains work. So either this is a bug in the compiler, or the ValueOf trick is not safe to use in PureScript. Which would be sad, because this library is quite powerful :)

[natefaubion]

The problematic instance resolution seems to happen in coerceFromF, where the second instance is always chosen despite the type constructor not being known to be different from Array.

This sounds like the usual apartness bug, which is probably fixed by purescript/purescript#4149.