{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FlexibleInstances, TypeFamilies, TypeOperators, DataKinds, StandaloneKindSignatures, FlexibleInstances, QuantifiedConstraints, FlexibleContexts, ConstraintKinds, KindSignatures, ScopedTypeVariables, UndecidableInstances, MultiParamTypeClasses, GADTs, ExistentialQuantification, TupleSections, NamedFieldPuns, UnicodeSyntax, PolyKinds, LambdaCase, PartialTypeSignatures, KindSignatures, TypeFamilyDependencies, UndecidableSuperClasses, FunctionalDependencies, ImpredicativeTypes, UnicodeSyntax, AllowAmbiguousTypes #-}
import Data.Either
type CSat = () :: Constraint
type CNSat = Int ~ Bool
type family OfKind a b where
OfKind a (b :: a) = CSat
OfKind a (b :: m) = CNSat
type family OfType a b where
OfType a a = CSat
OfType a b = CNSat
fu :: OfKind * t => t -> t
fu = id
_ = fu 0 -- Ok, Int is *
_ = fu Either -- OK???? WUTTTT????!!!!!! Either is * -> * -> *
The most fun answer is ‘why does this compile?’. It contradicts my intuition since I expect Either to not be *, do you know what is going on here?
Is it because with poly kinds haskell treats everything as *?
OfKind.hs:18:8: error:
• Data constructor not in scope: Either
• Perhaps you meant variable ‘either’ (imported from Prelude)
|
18 | _ = fu Either -- OK???? WUTTTT????!!!!!! Either is * -> * -> *
| ^^^^^^
The kind of (->) is * -> * -> * so all function arguments are always of kind *.
My reasoning was that when compiler solves OfKind * Either it obviously should reject it since Either is * -> * -> * and not *. Maybe it is caused by poly kinds, since the entire hierarchy is collapsed into everything being *.
it would appear to refer to a data constructor Either, not the type constructor. (Do you have -fdefer-type-errors or -defer-out-of-scope-variables enabled, or is there a data constructor Either in scope?) The type of a data constructor will always have kind *.
Perhaps you meant fu @Either? That should be rejected.
That will make your code work without errors. The type-level and term-level namespaces are separated so overlapping names are allowed. It is common to declare a type like this: data Test = Test which defines a type Test with a term constructor Test.
Functions can only take terms as arguments not types. The full type of fu is forall t. OfKind * t => t -> t you can use @ (aka type applications) to proved the concrete type of forall-quantified type variables explicitly. But then there is still the term argument of type t that you need to provide. So fu @Either has type OfKind * Either => Either -> Either which is not a valid type because the Eithers need more arguments.
Yes that was me.
The main thing I wanted to get info about was actually about this piece:
data HList :: [*] -> * where
Cons :: p -> HList a -> HList (p ': a)
End :: HList '[]
type CSat = () :: Constraint
type CNSat = Int ~ Bool
type family CCond a (b :: t) (c :: t) :: t where
CCond CSat a b = a
CCond CNSat a b = b
type family EachElementOfType a b where
EachElementOfType a '[] = CSat
EachElementOfType a (p : b) =
CCond (OfType a p) (EachElementOfType a b) CNSat
f :: EachElementOfType String t => HList t -> String
f v = let
recursor = \e acc -> case e of
Cons a b -> recursor b (acc ++ a)
End -> acc
in recursor v ""
_ = f (Cons "A" (Cons "B" (Cons "C" End)))
Compiler cannot derive from this that hlist contains only strings. Anyway I can specify it?
There are a couple of issues with the code you posted:
You need to give a type signature to recursor. In general, pattern matching on a GADT (such as HList) requires a type signature.
Your EachElementOfType family is defined rather strangely. Given EachElementOfType String (p : b) where the compiler knows nothing more about p, it will get stuck because it can’t simplify OfType String p. Instead you can say something like this:
type family EachElementOfType a b :: Constraint where
EachElementOfType a '[] = CSat
EachElementOfType a (p : b) = (a ~ p, EachElementOfType a b)
What are you actually trying to do, out of curiosity?
{-# LANGUAGE KindSignatures, PolyKinds, DataKinds, TypeOperators, GADTs, ConstraintKinds, TypeFamilies, UndecidableInstances, ScopedTypeVariables, RankNTypes, AllowAmbiguousTypes, TypeApplications, FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
import Data.Kind
import Data.Type.Equality
data HList :: [*] -> * where
Cons :: p -> HList a -> HList (p ': a)
End :: HList '[]
data Dict c where
Dict :: c => Dict c
class AllEq a as where
allEq :: forall b bs. Either (as :~: '[]) ((as :~: (b ': bs)) -> (b :~: a, Dict (AllEq a bs)))
instance AllEq a '[] where
allEq = Left Refl
instance AllEq a as => AllEq a (a ': as) where
allEq = Right (\Refl -> (Refl, Dict))
allEqTail :: forall a b c bs. AllEq a (b ': bs) => ((a ~ b, AllEq a bs) => c) -> c
allEqTail x = case allEq @a @(b ': bs) of
Right f -> case f Refl of
(Refl, Dict) -> x
f :: forall t. AllEq String t => HList t -> String
f v = let
recursor :: forall t'. AllEq String t' => HList t' -> String -> String
recursor = \e acc -> case e of
Cons (a :: tb) (b :: HList tbs) -> allEqTail @String @tb @String @tbs (recursor b (acc ++ a))
End -> acc
in recursor v ""
_ = f (Cons "A" (Cons "B" (Cons "C" End)))
type family EachElementOfType a b :: Constraint where
EachElementOfType a '[] = ()
EachElementOfType a (p : b) = (a ~ p, EachElementOfType a b)
f :: EachElementOfType String t => HList t -> String
f v = let
recursor :: EachElementOfType String t' => HList t' -> String -> String
recursor = \e acc -> case e of
Cons a b -> recursor b (acc ++ a)
End -> acc
in recursor v ""