Lysxia / first-class-families

First-class type families
https://hackage.haskell.org/package/first-class-families
MIT License
86 stars 12 forks source link

Question about Elem #23

Closed gspia closed 4 years ago

gspia commented 4 years ago

hi!

I was looking at Elem function (in List.hs) to use it and saw that it's definition is

data Elem :: a -> [a] -> Exp a
type instance Eval (Elem a as) = Eval (IsJust =<< FindIndex (TyEq a) as)

But the definition of IsJust is (in Common.hs)

data IsJust :: Maybe a -> Exp Bool
type instance Eval (IsJust ('Just _a)) = 'True
type instance Eval (IsJust 'Nothing) = 'False

which looks like that it would incompatible (or that Elem data sig is incompatible).

When trying out e.g.

:kind! Eval (Elem 1 '[1,2,3])
:kind! Eval (Elem 1 '[2,3])

it looks like that the Elem would not be evaluated. So the q is that should it be

data Elem :: a -> [a] -> Exp Bool

??

(I tried with that and then it evaluates.)

Lysxia commented 4 years ago

You're right! Good catch!

There should really be more tests so that every function is used at least once.

gspia commented 4 years ago

Yes