GitLab

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.