## 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) |