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
Loading comments…