Possible bug in apartness checking #3531
Description
Consider the following program:
module Main where
import Prelude
import Effect.Class.Console (log)
import Prim.TypeError (class Fail, Beside, Quote, Text)
class C x where
thing :: x -> x
data X a b = X
test1 :: forall a. X a Unit
test1 = X
instance cx :: C (X x x) where
thing = identity
else instance cxFail ::
Fail
(Beside
(Beside (Text "Fell through: x ~ ") (Quote x))
(Beside (Text ", y ~ ") (Quote y)))
=> C (X x y) where
thing = identity
main = do
let X = thing test1
log "Done"It fails to pass type checking, with the following error:
Compiling Main
[1/1 NoInstanceFound] src/Main.purs:28:7
28 let X = thing test1
^^^^^^^^^^^^^^^
A custom type error occurred while solving type class constraints:
Fell through: x ~ t1, y ~ Unit
while applying a function thing
of type C t0 => t0 -> t0
to argument test1
while inferring the type of thing test1
in value declaration main
where t0 is an unknown type
t1 is an unknown type
However, my understanding is that the cx instance should be selected, and that we should only be able to fall through to the next instance once we can ensure that the two type variable arguments to X are apart. In this case, they are not, since t1 could unify with Unit.