Surprising instance resolution

1

I discovered this while implementing instances of HasResponse for RespondAs. I’ve boiled it down to the following minimal example, which has to be split across 2 files, one of which has PolyKinds enabled and the other does not (the only other extensions enabled at the package level are ScopedTypeVariables and FlexibleInstances):

-- X.hs
{-# LANGUAGE PolyKinds #-}

module X where

data X p a

-- HasTypeRep.hs
module HasTypeRep where

import Data.Typeable
import X

class HasTypeRep a where
  getTypeRep :: Proxy a -> TypeRep

instance {-# OVERLAPPABLE #-} (Typeable a) => HasTypeRep a where
  getTypeRep = typeRep

instance {-# OVERLAPPING #-} (HasTypeRep a) => HasTypeRep (X p a) where
  getTypeRep _ = getTypeRep (Proxy :: Proxy a)

I know, careless overuse of OVERLAPPING is an easy way to weirdness, but anyway… Let’s load this in a repl, with DataKinds enabled (I’ve tested this with GHC 9.8.4):

-- works as intended
ghci> getTypeRep $ (Proxy :: Proxy (X () Int))
Int
ghci> getTypeRep $ (Proxy :: Proxy (X Char Int))
Int

-- until..
ghci> getTypeRep $ (Proxy :: Proxy (X 'True Int))
X Bool * 'True Int
ghci> getTypeRep $ (Proxy :: Proxy (X '() Int))
X () * '() Int
ghci> getTypeRep $ (Proxy :: Proxy (X '[Char] Int))
X [*] * (': * Char ('[] *)) Int

It seems that when the p type variable of X has kind Type, then GHC uses the second instance; but when it has any other kind, the first.

This can be easily solved by enabling PolyKinds in the HasTypeRep module, but I thought this was worth noting.

2 Likes
2

That is a common snag with polykinded type classes (or type families). They can match on a kind you don’t see.

Maybe there’s a warning to make of this, but I’m not sure what a good rule would be to avoid too many false positives. (Or maybe one could propose a simple rule with a convincing argument that what appear to be false positives are actually true positives.)

Another mitigating approach would be to provide better tools to visualize and understand what instance gets picked.

I brought that up once in a GHC issue and it turns out there’s an undocumented flag -ddump-cs-trace that kinda already does this. It just needs a bit of love to become a proper user-facing feature. This is a pretty low-hanging fruit for anyone looking to contribute a feature to GHC!

Here’s another issue on the same thing, and there’s probably a couple more if you dig around.

2 Likes
3

Thanks for the tip! This is the output I get with -ddump-cs-trace:

simplify_loop iteration=0 (definitely_redo = True, 0 simples to solve)
unif_happened False
simplify_loop iteration=0 (definitely_redo = True, 0 simples to solve)
Step 1[l:1,d:0] Kept inert DictCt:
    [G] $dHasTypeRep_aK1 {0}:: HasTypeRep a_aK0[sk:1]
simplify_loop iteration=0 (definitely_redo = True, 1 simples to solve)
Step 2[l:1,d:0] Dict equal [W] $dHasTypeRep_aK4 {0}:: HasTypeRep
                                                        a_aK0[sk:1] (CDictCan):
    [W] $dHasTypeRep_aK4 {0}:: HasTypeRep a_aK0[sk:1]
unif_happened False
unif_happened False
Constraint solver steps = 2
simplify_loop iteration=0 (definitely_redo = True, 0 simples to solve)
unif_happened False
simplify_loop iteration=0 (definitely_redo = True, 0 simples to solve)
Step 1[l:1,d:0] Kept inert DictCt:
    [G] $dHasTypeRep_aKB {0}:: HasTypeRep a_aKz[ssk:1]
simplify_loop iteration=0 (definitely_redo = True, 0 simples to solve)
simplify_loop iteration=0 (definitely_redo = True, 1 simples to solve)
Step 2[l:2,d:0] Dict equal [W] $dHasTypeRep_aKI {0}:: HasTypeRep
                                                        a_aKz[ssk:1] (CDictCan):
    [W] $dHasTypeRep_aKI {0}:: HasTypeRep a_aKz[ssk:1]
unif_happened False
unif_happened False
Step 3[l:1,d:0] Kept inert DictCt:
    [G] $dTypeable_aL1 {0}:: Typeable a_aL0[ssk:1]
simplify_loop iteration=0 (definitely_redo = True, 0 simples to solve)
simplify_loop iteration=0 (definitely_redo = True, 1 simples to solve)
Step 4[l:2,d:0] Dict equal [W] $dTypeable_aLa {0}:: Typeable
                                                      a_aL0[ssk:1] (CDictCan):
    [W] $dTypeable_aLa {0}:: Typeable a_aL0[ssk:1]
unif_happened False
unif_happened False
unif_happened False
Constraint solver steps = 4
Step 1[l:0,d:0] Kept inert DictCt:
    [G] pm_dLq_dLq {0}:: HasTypeRep a_aKz
Constraint solver steps = 1
Step 1[l:0,d:0] Kept inert DictCt:
    [G] pm_dLs_dLs {0}:: HasTypeRep a_aKz
Constraint solver steps = 1
Step 1[l:0,d:0] Kept inert DictCt:
    [G] pm_dLv_dLv {0}:: Typeable a_aL0
Constraint solver steps = 1
Step 1[l:0,d:0] Kept inert DictCt:
    [G] pm_dLx_dLx {0}:: Typeable a_aL0
Constraint solver steps = 1

Not really sure what I’m looking at here.

4

I think that’s the trace from typechecking your file HasTypeRep.hs, which isn’t that interesting. Instead you can enable the flag after loading your file.

$ ghci -XHaskell2010 -XDataKinds -XFlexibleInstances -XScopedTypeVariables HasTypeRep.hs
ghci> :set -ddump-cs-trace
ghci> getTypeRep $ (Proxy :: Proxy (X () Int))
...
(trace 1)
...
ghci> getTypeRep $ (Proxy :: Proxy (X 'True Int))
...
(trace 2)
...

The output is very noisy, but notice these lines in the trace of getTypeRep $ (Proxy :: Proxy (X () Int)):

Step 1[l:1,d:0] Dict/Top (solved wanted):
    [W] $dHasTypeRep_a1cN {0}:: HasTypeRep (X () Int)
Step 2[l:1,d:1] Dict/Top (solved wanted):
    [W] $dHasTypeRep_a1d5 {1}:: HasTypeRep Int
Step 3[l:1,d:2] Dict/Top (solved wanted):
    [W] $dTypeable_a1d6 {2}:: Typeable Int

which shows the succession of subgoals HasTypeRep (X () Int), HasTypeRep Int, Typeable Int, which, one can infer, comes from applying the OVERLAPPING instance in Step 1 before the OVERLAPPABLE instance in Step 2.

Compare that to the second trace, for getTypeRep $ (Proxy :: Proxy (X 'True Int)), which shows:

Step 1[l:1,d:0] Dict/Top (solved wanted):
    [W] $dHasTypeRep_a133 {0}:: HasTypeRep (X True Int)
Step 2[l:1,d:1] Dict/Top (solved wanted):
    [W] $dTypeable_a13l {1}:: Typeable (X True Int)
Step 3[l:1,d:2] Dict/Top (solved wanted):
    [W] $dTypeable_a13m {2}:: Typeable (X True)
Step 4[l:1,d:3] Dict/Top (solved wanted):
    [W] $dTypeable_a13o {3}:: Typeable X
Step 5[l:1,d:4] Dict/Top (solved wanted):
    [W] $dTypeable_a13q {4}:: Typeable Bool
...
(etc.)

which comes from applying the OVERLAPPABLE instance in the first step to get Typeable (X True Int), followed by the resolution of that Typeable goal in the remaining steps.

This flag is really intended for people working on GHC itself. To adapt it for normal users, one would have to reduce the noise (hide irrelevant details) and increase the signal (explain what each step is doing, which instances are picked and why others are discarded).

5

Interesting. Does this represent a bug in the constraint solver? I’m not familiar with how it’s implemented, but I had assumed that an OVERLAPPING instance would always take precedence over an OVERLAPPABLE one.

6

With PolyKinds on in module X, you declare:

data X @k @l (p :: k) (a :: l)

If you also enabled it in module HasTypeRep, then the overlapping instance would be:

instance {-# OVERLAPPING #-} forall k l (p :: k) (a :: l).
  HasTypeRep a => HasTypeRep (X @k @l p a)

alas, without it the instance is:

instance {-# OVERLAPPING #-} forall (p :: *) (a :: *).
  HasTypeRep a => HasTypeRep (X @* @* p a)

This instance head simply does not match X @Bool @* True Int, so GHC can only select the other one.

2 Likes