-
-
Save acowley/a001bd092599b5914bad to your computer and use it in GitHub Desktop.
Odd type checker error message
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE ConstraintKinds, DataKinds, GADTs, TypeFamilies, TypeOperators #-} | |
import Data.List (intercalate) | |
import Data.Proxy | |
import GHC.Prim (Constraint) | |
data HList :: [*] -> * where | |
Nil :: HList '[] | |
Cons :: a -> HList as -> HList (a ': as) | |
type family HListAll (c :: * -> Constraint) (ts :: [*]) :: Constraint where | |
HListAll c '[] = () | |
HListAll c (t ': ts) = (c t, HListAll c ts) | |
showHList :: HListAll Show ts => HList ts -> String | |
showHList = ("[" ++ ) . (++"]") . intercalate ", " . go | |
where go :: HListAll Show ts => HList ts -> [String] | |
go Nil = [] | |
go (Cons x xs) = show x : go xs | |
-- Things work okay up to this point | |
test :: String | |
test = showHList (Cons (2::Int) | |
(Cons (3.1 :: Float) | |
(Cons 'c' Nil))) | |
-- Now let's involve a type family indexed by a type that gives us our | |
-- constraint. | |
type family ConFun (t :: *) (a :: *) :: Constraint | |
data Tag | |
type instance ConFun Tag a = (Show a, Eq a, Ord a) | |
-- This is notionally similar to showHList | |
bar :: HListAll (ConFun l) ts => Proxy l -> HList ts -> () | |
bar _ _ = () | |
{- | |
This (baz) doesn't type check with the surprising error: | |
Could not deduce (ConFun l a, ConFun l b) | |
arising from a use of ‘bar’ | |
from the context (ConFun l a, ConFun l b) | |
bound by the type signature for | |
baz :: (ConFun l a, ConFun l b) => Proxy l -> HList '[a, b] -> () | |
-} | |
-- baz :: (ConFun l a, ConFun l b) => Proxy l -> HList [a,b] -> () | |
-- baz = bar |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment