Why does GHC 8.0.1 reject this programme?
The following programme compiles just fine with GHC 7.10.3 but GHC 8.0.1 rejects it with:
test.hs:23:13: error:
• Couldn't match type ‘("x" == "x") || ("x" == "y")’ with ‘'True’
arising from a use of ‘foo’
• In the expression: foo (MyType :: MyType '["x", "y"])
In a pattern binding: _ = foo (MyType :: MyType '["x", "y"])
In the expression:
do { let _ = foo (MyType :: MyType '["x", "y"]);
return () }
Could anyone please explain why? Thanks!
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Main where
import Data.Type.Bool
import Data.Type.Equality
type family Contains x xs where
Contains x '[] = 'False
Contains x (hd ': tl) = x == hd || Contains x tl
foo :: (Contains "x" xs ~ 'True) => MyType xs -> ()
foo = const ()
data MyType xs = MyType
main :: IO ()
main = do
let _ = foo (MyType :: MyType '["x", "y"])
return ()
Posted May 29, 2016, 7:21 PM UTC
31