Type family, pattern not matching

This is a follow up to issue #9898. The partially applied type families have been eliminated yet type checking is still failing.

It is expected that 'test1' infer as (Char, ()) but it does not. It seems that GHC is not matching the correct pattern on :$:. 'test3' and 'test4' indicate that GHC sometimes matches the correct pattern.

'test2' demonstrates an inconsistency between type checking with GHC and the type checking that occurs when the same expression is entered in GHCi. I do not know if this is a related problem. Enabling AllowAmbiguousTypes suggests it might be related because the compiler then complains ApplyFilter (ToBool ((:.:) Not (Equal Char) Char)) (Char, ()) cannot be unified with () (With the second :$: rule enabled).

Reported type of 'test1' with second rule removed

test1
  :: (Char,
      ApplyFilter (ToBool ((Not :.: Equal Char) :$: Char)) (Char, ()))

Reported type of 'test1' with second rule added

test1
  :: (Char,
      ApplyFilter (ToBool ((:.:) Not (Equal Char) Char)) (Char, ()))

test2 type check error

ghc_bug3.hs:38:15:
    Couldn't match expected type ‘ApplyFilter
                                    (ToBool ((Not :.: Equal Char) :$: Char)) (Char, ())’
                with actual type ‘ApplyFilter
                                    (ToBool ((Not :.: Equal Char) :$: Char)) (Char, ())’
    NB: ‘ApplyFilter’ is a type function, and may not be injective
    The type variables ‘k0’, ‘k1’, ‘k2’ are ambiguous
    In the ambiguity check for:
      forall (k :: BOX) (k1 :: BOX) (k2 :: BOX).
      ApplyFilter (ToBool ((Not :.: Equal Char) :$: Char)) (Char, ())
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In an expression type signature:
      ApplyFilter (ToBool ((Not :.: Equal Char) :$: Char)) (Char, ())
    In the expression:
        () ::
          ApplyFilter (ToBool ((Not :.: Equal Char) :$: Char)) (Char, ())

{-# LANGUAGE TypeFamilies, GADTs, DataKinds, UndecidableInstances, TypeOperators, PolyKinds #-}
module Main where

data Equal x y
data Not x

type family ToBool x where
  ToBool (Equal x x) = True
  ToBool (Equal x y) = False
  ToBool (Not True) = False
  ToBool (Not False) = True
  ToBool (Not p) = ToBool (Not (ToBool p))

data (:.:) g f x
infixr 9 :.:

type family f :$: x where
  (g :.: f) :$: x = g (f x)
-- Uncomment to see change in 'test1' -- f :$: x = f x

type family Filter f l where
  Filter f (x, xs) = ApplyFilter (ToBool (f :$: x)) (x, Filter f xs)
  Filter f () = ()

type family ApplyFilter p xs where
  ApplyFilter False (x, xs) = xs
  ApplyFilter p xs = xs

type family xs :+: ys where
  (x, xs) :+: ys = (x, xs :+: Filter (Not :.: Equal x) ys)
  () :+: ys = ys
infixl 5 :+:

test1 = undefined :: (Char, ()) :+: (Char, ())

-- Typing this into GHCi works fine, but here does not type check.
test2 = () :: ApplyFilter (ToBool ((Not :.: Equal Char) :$: Char)) (Char, ())

-- Type checks (with second rule added)
test3 :: Maybe :$: Int
test3 = Just 5

-- Type checks
test4 :: (Maybe :.: Maybe) :$: Int
test4 = Just (Just 5)

Trac metadata

Trac field	Value
Version	7.8.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture