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