Pure unifier is incomplete around casts and AppTys: instance lookup fails
The pure unifier (in GHC.Core.Unify
) is incomplete with respect to casts. Here is the counter-example:
alpha :: Type -> Type -- this is the template variable
a :: Type -> k
co :: k ~ Type
(alpha Int) ~? (a Int |> co)
Today, the pure unifier will claim that these two types have no unifier. But they do:
alpha :-> a |> <Type> -> co
This, unfortunately, will not be easy to solve. We will have to somehow remember the casts that we see as we descend into a type, and use those casts for rewriting.
Here is a concrete program that witnesses the problem:
{-# LANGUAGE FlexibleInstances, TypeFamilies, ExplicitForAll, KindSignatures,
DataKinds #-}
module Bug where
import Data.Kind ( Type )
class C a where
meth :: a -> ()
instance C (b Int) where
meth _ = ()
type family Star where
Star = Type
f :: forall (c :: Type -> Star). c Int -> ()
f x = meth x
As written, it fails with
Bug.hs:17:7: error:
• No instance for (C (c Int)) arising from a use of ‘meth’
• In the expression: meth x
In an equation for ‘f’: f x = meth x
|
17 | f x = meth x
| ^^^^^^
But change the type of c
to become Type -> Type
, and the program is accepted.