Oddity of type checker or bug?

Chat
#1

Don’t look too much into what this code does, it’s just a small example of the behavior I was a little surprised at.

Two implementations of anyShow, one using TypeEquals and the other not. Sometimes they act the same, and sometimes they don’t. I’m guessing test4 works fine because it’s at the top level, whereas in test6 it is not, and the bidirectional type checker is doing something different for each as there’s different contexts?

module Main where

import Prelude

import Unsafe.Coerce
import Type.Proxy
import Type.Equality

anyShow1 :: forall a. Proxy a -> (Show a => String) -> String
anyShow1 _ f = (coerce f) { show: \_ -> "Shown" }
  where
    coerce :: (Show a => String) -> ({ show :: a -> String } -> String)
    coerce = unsafeCoerce
    
anyShow2 :: forall a x. TypeEquals x (Show a => String) => Proxy a -> x -> String
anyShow2 _ f = (coerce f) { show: \_ -> "Shown" }
  where
    coerce :: x -> ({ show :: a -> String } -> String)
    coerce = unsafeCoerce

data V = V

test1 = anyShow1 (Proxy :: _ V)

-- same type inferred for test2 as test1
test2 = anyShow2 (Proxy :: _ V)

test3 = test1 (show V)

test4 = test2 (show V)

test5 = anyShow1 (Proxy :: _ V) (show V)

-- doesn't work
--   Could not match constrained type `Show V => String` with type `String`
-- test6 = anyShow2 (Proxy :: _ V) (show V)

-- but does work with an explicit annotation
test7 = (anyShow2 (Proxy :: _ V) :: (Show V => String) -> String) (show V)
#2

I think it’s an issue of the order of instances being resolved, so my guess is:

When passing show V into anyShow2, the typechecker assumes that the RHS of constraints is what was intended to be passed in, as it only sees the vague type variable x, and thus implies String ~ x

But then it tries to solve TypeEquals, and that implies (Show V => String) ~ x. So really there are two errors, not being able to match Show V => String with String, and no instance found for Show V

#3

Your intuition is correct. In the compiler typechecking/elaboration happens before constraint solving. It will use information from anyShow to decide how to elaborate show V. When it has a concrete type to latch on to Show V => String (like anyShow), it knows that it should elaborate show V to include a function argument accepting the Show V dictionary. TypeEquals defers something to the constraint solver. There’s nothing special about TypeEquals. To the compiler it’s just an arbitrary constraint. It’s not a primitive constraint or anything, like in GHC. All the typechecker is seeing then is that it should be x as chosen by the caller. Without an additional signature, the compiler sees show V as String. It then instantiates the signature of anyShow2 with String as x. It then gets kicked to the constraint solver, where it tries to solve TypeEquals String (Show a => String), which cannot be solved.

The behavior here is correct. We must know all the constraints to search for before we can start searching for them! Elaboration must happen before constraint solving. In general, constraint solving does not work to compute polytypes. If you tried to write an instance for something, and used a constrained type in an instance head, I believe the compiler would reject it. I think the real issue is that it should probably reject the constrained type in the TypeEquals RHS.

3 Likes