GitLab

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.