Wanted: higher-order type-level programming

'test3' is expected to type check given that 'test1' and 'test2' type check. 'test4' is not expected to type check.

ghc_bug2.hs:24:9:
    Couldn't match type `(Char, ())' with `()'
    Expected type: Filter (Equal Int) (Char, Filter (Equal Int) ())
      Actual type: ()
    In the expression:
        () :: Filter (Equal Int) (Char, Filter (Equal Int) ())
    In an equation for `test2':
        test2 = () :: Filter (Equal Int) (Char, Filter (Equal Int) ())

ghc_bug2.hs:28:9:
    Couldn't match type `(Char, ())' with `()'
    Expected type: Filter (Equal Int) (Char, ())
      Actual type: ()
    In the expression: ()
    In an equation for `test3': test3 = ()

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

type family Filter f xs where
  Filter f (x, xs) = ApplyFilter (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 Equal x y where
  Equal x x = True
  Equal x y = False
--

-- Type checks
test1 :: ApplyFilter ((Equal Int) Char) (Char, Filter (Equal Int) ())
test1 = ()

-- Couldn't match type `(Char, ())' with `()'
test2 = () :: Filter (Equal Int) (Char, Filter (Equal Int) ())

-- Couldn't match type `(Char, ())' with `()'
test3 :: Filter (Equal Int) (Char, ())
test3 = ()

-- Type checks, should not
test4 :: Filter (Equal Int) (Char, ())
test4 = ('x', ())

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	Windows
Architecture	x86_64 (amd64)