Surprising specialisation with INCOHERENT and rank 2 types

changed the description

I strongly suspect the mechanism here is basically the same as #16586 (closed). Note [NOINLINE withSomeSNat] may be an interesting read.

In your reproducer, you want this function...:

newProcess
  :: (forall p. Process main p -> Kahn main (p:ps) a)
  -> Kahn main ps a

...to effectively call its argument with a different process tag p every time it is invoked. But in the actual implementation, the type p is completely unconstrained and as a result it will be defaulted to Any @Type every time, rather than to a unique-for-every-call skolem. And after inlining, the specializer will be able see that actually all of the process tags in the program are the same: Any @Type. Finally, the specializer assumes that all instances of Any @Type <: (Any @Type : Any @Type : '[]) are interchangeable, when in fact we have one instance that comes from p <: (p : q : '[]) with index = Z and another that comes from q <: (p : q : '[]) with index = S Z, which are not really interchangeable.

@clyring That does look to be the case.

To summarise, if I understand correctly:

Because GHC lacks truly distinct skolems, they're all ultimately instantiated to the same type.
Inlining allows the specialiser to witness this infelicitous fact and thus blunder on overloaded functions.
The workarounds are:
- The as yet unimplemented runExists (#19675).
- To NOINLINE anything that binds new types for which instance resolution will take place.
- To manufacture and instantiate unique types manually.

I took a couple stabs at this, but I don't know GHC internals so they may be naive.

{-# LANGUAGE MagicHash, TypeData, TypeFamilies, UnboxedTuples #-}
{-# LANGUAGE RoleAnnotations, BlockArguments #-}

module Fresh (

  -- * With Global Mutable State

  runExists,
  runExistsIO,

  -- * With an Indexed Monad

  PST, runPST,
  S, runExistsPST,
  pstToST, liftST,
  pstToIO, liftIO,
  ipure, ibind,

) where

import GHC.Exts (Proxy#, proxy#, State#, RealWorld)
import GHC.ST (ST(..), runST)
import GHC.IO (IO(..))
import System.IO.Unsafe (unsafePerformIO)
import Data.IORef (IORef, newIORef, readIORef, writeIORef)


type data Nat = Z | S Nat

type family Any (n :: Nat) :: k where {}

data SomeNat where
  SomeNat :: {-# UNPACK #-} !(Proxy# @Nat n) -> SomeNat

{-# NOINLINE source #-}
source :: IORef SomeNat
source = unsafePerformIO do
  newIORef (SomeNat (proxy# @Z))

runExists :: (forall (t :: k). Proxy# t -> r) -> r
runExists k = unsafePerformIO do
  runExistsIO \p ->
    pure (k p)

runExistsIO :: (forall (t :: k). Proxy# t -> IO r) -> IO r
runExistsIO k = do
  SomeNat (_ :: Proxy# n) <- readIORef source
  writeIORef source (SomeNat (proxy# @(S n)))
  k (proxy# @(Any n))


type role PST nominal nominal nominal representational
newtype PST s (i :: Nat) (j :: Nat) a
  = PST{ unPST :: Proxy# i -> State# s -> (# Proxy# j, State# s, a #) }

runPST :: (forall s. PST s i j a) -> a
runPST pst = runST (pstToST pst)

runExistsPST :: (forall (t :: k). Proxy# t -> PST s (S i) j r) -> PST s i j r
runExistsPST k = PST \(_ :: Proxy# i) s -> unPST
  (k (proxy# @(Any i)))
  (proxy# @(S i))
  s

pstToST :: PST s i j a -> ST s a
pstToST (PST ija) = ST \s -> case ija proxy# s of
  (# _, s', a #) -> (# s', a #)

liftST :: ST s a -> PST s i i a
liftST (ST f) = PST \p s -> case f s of
  (# s', a #) -> (# p, s', a #)

pstToIO :: PST RealWorld i j a -> IO a
pstToIO (PST ija) = IO \rw -> case ija proxy# rw of
  (# _, rw', a #) -> (# rw', a #)

liftIO :: IO a -> PST RealWorld i i a
liftIO (IO f) = PST \p rw -> case f rw of
  (# rw', a #) -> (# p, rw', a #)

ipure :: a -> PST s i i a
ipure x = PST \p s -> (# p, s, x #)

ibind :: PST s i j a -> (a -> PST s j k b) -> PST s i k b
ibind (PST ija) aFjkb = PST \i s -> case ija i s of
  (# j, s', a #) -> unPST (aFjkb a) j s'

Not sure what the costs are like, relative to NOINLINE. Actually, I'm not sure the first stab even works; I can't test it against my brittle reproducer since the noise of its introduction alone is enough to scare away the bug.

Does the problem go away with -fno-specialise-incoherents? This sounds like #22448 (closed).

The most obvious solution to me would be to have pragmas to mark classes which are not expected to be coherent. The specialiser would then be able to refrain from specialising them. At the moment, if you use INCOHERENT instances which have different dictionaries, the compiler makes few guarantees that it will not arbitrarily choose one or the other.

@adamgundry Nope. I forgot about it in the meantime (or I would have mentioned this flag), but I actually found that issue days ago when I first looked for a preexisting bug report.

The thing is, instance resolution for the class in question isn't actually expected to exhibit any incoherence. The INCOHERENT instance (which would just be OVERLAPPING in typical usage with concrete types) is needed for GHC to proceed with resolution when all the types involved are skolems.

(to clarify what I failed to mention in my previous comment: {-# NOINLINE newProcess #-} does indeed work)

Okay, that's interesting. Perhaps #23429 (closed) is also relevant.

The thing is, instance resolution for the class in question isn't actually expected to exhibit any incoherence.

There are two possible interpretations of the term "incoherence":

Type inference can make arbitrary choices
The program constructs two dictionaries with the same type but observably different values

I think you are saying that your program does not exhibit the first (because there is only one INCOHERENT instance, and it overlaps the other instance, so there is always a canonical most-specific choice). But this property is not stable under substitution, so it does exhibit incoherence in the second sense (namely different dictionaries of type Any @Type <: (Any @Type : Any @Type : '[])).

runExists makes sense if the dictionary really is a singleton type, like SSymbol, and we merely need to conjure an existential because we don't know statically what the value will be. But the situation in this ticket is different, because the dictionary is not a singleton. So I think the Right Thing would be to tag the class as being non-singleton, if only we had such a mechanism...

(Maybe another possibility would be to make the dictionaries genuine singletons, which would require apartness constraints ala #17585, to say something like instance (x <: xs, x /~ y) => x <: (y:xs) where index = S index. But that seems more complex.)

@adamgundry In the context of my usage at least, the types in the list are (supposed to be) unique, so you can consider the dictionaries to be singletons.

runExists should be the best workaround, but I think the true solution here is for GHC to avoid unintended collisions by defaulting the unrestricted types to distinct instances of type family Any (n :: Nat) :: k where {}.

Edit: GHC already has a lot of machinery for generating and maintaining fresh names. Perhaps it can be applied to these distinguishable Anys?

Edit 2: Continuing this thought, if we instead have something like type family Any (n :: Name) :: k where {}, then when GHC sees unrestricted forall a. ... (forall a. ...) it can instantiate the first to Any (Name "a" 0) and the second to Any (Name "a" 1) (or whatever). If these get inlined somewhere, renaming can handle the collisions.

Edit 3: I guess an equivalent solution is "just don't default" or "default at the very end"—let your tyvars stay tyvars. Is this tenable?

added Tbug label

added Pnormal label and removed Tbug label

added Tbug label

removed needs triage label

added typechecker label

added IncoherentInstances label

removed IncoherentInstances label

added IncoherentInstances label

runExists should be the best workaround, but I think the true solution here is for GHC to avoid unintended collisions by defaulting the unrestricted types to distinct instances of type family Any (n :: Nat) :: k where {}.

Before discussing possible solutions, I'd love to understand the problem. In the light of the above discussion, is it possible to make a small repro case that illustrates the problem in high relief? As it stands there is quite a lot of code, and I don't know what the problem is, exactly. Thanks!

@simonpj Behold:

{-# LANGUAGE DataKinds, GADTs, RoleAnnotations #-}

--import GHC.Exts (Any)
import Data.Proxy


main :: IO ()
main = run $
  False `byProxy` \p1 ->
  True  `byProxy` \p2 -> \hl -> do
    putStrLn $ show (infer hl `matching` p1)
            ++ " <-- should be " ++ show (Handle False)
    putStrLn $ show (infer hl `matching` p2)
            ++ " <-- should be " ++ show (Handle True)


data HList f xs where
  Nil  :: HList f '[]
  (:~) :: f x -> HList f xs -> HList f (x:xs)

data Index x xs where
  Z :: Index x (x:xs)
  S :: Index x xs -> Index x (y:xs)

class                                    x <:    xs  where index :: Index x xs
instance {-# INCOHERENT   #-}            x <: (x:xs) where index = Z
instance {-# OVERLAPPABLE #-} x <: xs => x <: (y:xs) where index = S index

--{-# SPECIALISE infer :: forall k a. HList (Handle a) [Any @k, Any @k]
--                     -> Handle a (Any @k)
-- #-}
infer :: x <: xs => HList f xs -> f x
infer xs = xs ! index
 where
  (!) :: HList f xs -> Index x xs -> f x
  y :~ _  ! Z   = y
  _ :~ ys ! S i = ys ! i
  Nil     ! i   = case i of

matching :: f x -> proxy x -> f x
fx `matching` _ = fx


type role Handle representational nominal
newtype Handle a s = Handle a
  deriving Show

run :: (HList f '[] -> r) -> r
run f = f Nil

--{-# NOINLINE byProxy #-}
byProxy
  :: a
  -> (forall x. Proxy x -> HList (Handle a) (x:xs) -> r)
  -> HList (Handle a) xs -> r
x `byProxy` k = \xs -> k Proxy (Handle x :~ xs)

Uncomment the SPECIALISE or NOINLINE pragmata to see the other two outcomes.

Though for understanding the problem, I'm pretty sure @clyring already hit the nail on the head: I've run into the very issue that runExists was conceived to address. It goes like this:

We use rank-2 polymorphism to introduce "new", "unique" types for tagging handles that must never be mixed up.
We keep a heterogeneous list of these handles in context so that the user doesn't have to supply them all manually when the type can be inferred.
The task of projecting out the right handle is given to the <: class, which we reason in this limited context can only select the correct instance, INCOHERENT notwithstanding.
But when byProxy is inlined, the unconstrained tyvars liberated from its body are revealed to have been replaced by none other than Any!
Gasp. By speaking aloud that dreaded name, we've summoned the specialiser.
"About these dictionaries of yours..." It smirks. "They, uh, have the same type, don't they?"

Thanks for the nice minimized example @LSLeary!

The task of projecting out the right handle is given to the <: class, which we reason in this limited context can only select the correct instance, INCOHERENT notwithstanding.

This is the subtle bit. The <: class is by itself dangerous, because it violates global coherence (i.e. INCOHERENT is behaving as expected). We try to safely encapsulate it via rank-2 polymorphism, but fail because of the lack of something like runExists and the fact that Anys used for defaulting are interchangeable.

(Side note: I'm sure there was a recent ticket discussing issues in the pattern-match checker where Any was causing problems, but I now can't find it. Can anyone? Perhaps that's more motivation for an approach where all Anys are distinct.)

But I continue to think that in this specific example, a cleaner solution would be to mark the <: class as not globally coherent (and hence not specialisable). That would make it safe to use without the (difficult to enforce) constraint about the list containing no duplicates.

(Side note: I'm sure there was a recent ticket discussing issues in the pattern-match checker where Any was causing problems, but I now can't find it. Can anyone? Perhaps that's more motivation for an approach where all Anys are distinct.)

Indeed! #24817 (closed) I'm curious to see what the solution to this ticket is; it might well fix #24817 (closed) as well.

I haven't comprehended the reproducer yet, but both the Specialiser as well as the pattern-match checker are affected by the ... erasure ("strange skolemnisation") of existentials to a single Any.

marked this issue as related to #24817 (closed)

marked this issue as related to #16586 (closed)

marked this issue as related to #19675

changed title from INCOHERENT Violates Type Safety to Surprising specialisation with INCOHERENT and rank 2 types

Does the problem go away with -fno-specialise-incoherents? This sounds like #22448 (closed).

@adamgundry Nope. I forgot about it in the meantime (or I would have mentioned this flag), but I actually found that issue days ago when I first looked for a preexisting bug report.

That sounds like a bug in -fno-specialise-incoherents to me. Should we split out a separate ticket for that sub-issue or just track it here as well?

I think this may be (related to) #23429 (closed). (EDIT: or maybe #23560?)

Although having said that, I can't seem to reproduce the misbehaviour using the module above on 9.8.1 or 9.10.0.20240426 with -fno-specialise-incoherents (though it does reproduce without it).

marked this issue as related to #23429 (closed)

marked this issue as related to #23560

marked this issue as related to #23831

added specialisation label

changed the description

Surprising specialisation with INCOHERENT and rank 2 types

Summary

Steps to reproduce

Expected behavior

Environment

Child items ...

Activity

Surprising specialisation with INCOHERENT and rank 2 types

Summary

Steps to reproduce

Expected behavior

Environment

Relates to

Activity