GHC's failure to rewrite in coercions & kinds leads to spurious occurs-check failure
Consider this mess:
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies,
StandaloneKindSignatures, AllowAmbiguousTypes, GADTs,
TypeOperators #-}
module Bug where
import Data.Kind ( Type )
import Data.Type.Equality ( type (~~) )
import Data.Proxy ( Proxy )
type Const :: () -> k1 -> k2 -> k1
type family Const u x y where
Const '() x y = x
type Equals :: k1 -> k2 -> Type
type family Equals a b where
Equals a a = Char
Equals a b = Bool
type IsUnit :: () -> Type
data IsUnit u where
ItIs :: IsUnit '()
f :: forall (u :: ()) (a :: Type) (b :: Const u Type a). (a ~~ b)
=> IsUnit u -> a -> Proxy b -> Equals a b
f ItIs _ _ = 'x'
g = f ItIs
GHC fails (in the RHS of g
) with an occurs-check, but it should succeed.
The problem is that we end up with
[W] (alpha :: Type) ~# (beta :: Const upsilon Type alpha)
where we have already unified upsilon := '()
.
But GHC refuses to rewrite in kinds, so the Const
never reduces, and we reject the program. Note that a solution exists, with alpha := Any @Type
and beta := Any @Type |> sym (AxConst Type (Any @Type))
.
Proposed solution:
The wanted above actually gets simplified to become
[W] co :: Const '() Type alpha ~# Type
[W] w2 :: (alpha :: Type) ~# ((beta |> co) :: Type)
The co
is easily solved. Then, when we get to w2
, we are in Wrinkle (3) of Note [Equalities with incompatible kinds]. Happily, we should be able to detect that alpha
is free in co
and reorient, giving
[W] w3 :: (beta :: Const '() Type alpha) ~# (alpha |> sym co :: Const '() Type alpha)
which can be solved by unifying beta := alpha |> sym co
. alpha
will then remain unconstrained and will be zonked to Any
.
The key new part is looking at the coercion when deciding whether to reorient.