Missed specialisation opportunity with phantom type class parameter?

I am unsure of my analysis of this code fragment. It seems like we could do a better job optimising test3. First the code, then the analysis at the bottom.

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE IncoherentInstances #-}
module Foo where

data Proxy a = Proxy

--type role Phantom phantom nominal

class Phantom x a | a -> x where
  method :: a
  method1 :: a

instance Phantom x (Proxy x) where
  method = Proxy
  method1 = Proxy

-- This doesn't optimise

test3 :: Phantom x (Proxy x) => Proxy x
test3 = method

-- This does optimise

instance Phantom Char Int where
  method = 5
  method1 = 5

test4 :: Phantom x Int => Int
test4 = method

Here is the relevant part of the core

-- RHS size: {terms: 4, types: 9, coercions: 0}
test3
test3 = \ @ x_ayL $dPhantom_ayS -> method $dPhantom_ayS

-- RHS size: {terms: 3, types: 5, coercions: 0}
test4
test4 = \ @ x_ayz _ -> $cmethod1_az4

In test4 the dictionary selector method is eliminated but in the analogous case test3 where x is used in both arguments then method is not specialised. It seems that we could do a similar specialisation and ultimately replace the dictionary with Proxy as x is phantom.

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	danharaj
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

We discovered this while analyzing a moderately large production system based on reflex and reflex-dom compiled with ghcjs. Web applications that use this framework rely heavily on specialization in order to be performant when run in a browser. One feature of reflex-dom is a javascript FFI facility built to allow uniform interaction with either ghcjs's low-level JS FFI or a native JS engine (such as WebKit) when built with ghc. This type class is the user interface for this feature:

class (Monad m, MonadIO (JSM m), MonadFix (JSM m), MonadJS x (JSM m)) => HasJS x m | m -> x where
  type JSM m :: * -> *
  liftJS :: JSM m a -> m a

The x parameter is important. There are situations where a program will manage multiple Javascript execution contexts. In general, references cannot be shared between execution contexts. So this is a slightly more elaborate version of the phantom type parameter used by the ST monad. The x parameter is used by the implementation of the FFI to tag various JS datastructures so that they cannot be intermixed: It guarantees this aspect of semantic correctness.

Unfortunately, using this FFI via HasJS prevents automatic specialization because even though the dictionary for HasJS need not depend on x in an essential way, GHC seems unable to automatically create a specialized version of a polymorphic declaration that is constrained by HasJS and marked INLINABLE. I believe this is because, according to the documentation in the Specialise module, the invariant of the specialiser for generated specialisations is that "no specialised version is overloaded" and GHC cannot deduce that the overloading caused by x is benign.

The workaround was to create an escape hatch that allowed the user to specify a concrete dummy type for x at the top-level, namely (). This allowed GHC to specialize all of their code which led to significant performance gains. This isn't the best situation: a user had to abandon type discipline ensuring semantic correctness in order to avoid unacceptable performance overhead.

Matthew: this is a rather odd case. Look at test4. We have a Wanted constraint [W] Phantom x0 Int, where x0 is a unification variable. But what is x0? We can use functional dependencies to get TWO derived constraints:

1. From the given [G] Phantom x Int, we get [D] x0 ~ x.
2. From the top-level instance Phantom Char Int, we get [D] x0 ~ Char.

GHC chooses one of these arbitrarily. If it chooses (2) we unify x0 := Int, and solve the constraint from the top-level instance. The given constraint is not used. We get nice efficient code.

But if it chooses (2) it'll unify x0 := x, and solve the wanted constraint from the given one, which is passed as a paramter to test4. That's less efficient.

But you set up this situation, by providing two places to solve the constraint: from the passed-in givens, or from a top level instance. Just give a simpler type signature test4 :: Int.

It's bit similar with test3. Again there are two ways to solve the wanted constraint: from the top-level instance or from the passed-in given.

I'm not inclined to lose sleep over all this, unless you have a compelling use-case.

---

danharaj: I think you are describing an entirely different problem. Could you make a reproducible test case?

added Pnormal label

mentioned in issue #17366 (closed)

added specialisation label