Do constraint checking influence typing correctness?

Learn
#1

I have this code:

{-# 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 *?

1 Like
#2

I’m getting:

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 *.

#3

I have Either imported from Prelude, weirdly enough. Perhaps, importing it explicitly should help import Data.Either

I have a few extensions enabled. Updated the post.

#4

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 *.

#5

I’m still getting the same error. Are you sure that that is the whole file because I also need to add import Data.Kind to get Constraint.

#6

When you write this:

_ = fu Either

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.

1 Like
#7

I don’t have anything else named Either, because it would cause a compilation error, wouldn’t it?

I expect that fu can take anything, including type constructors. It still complaints about the absence of parameters with fu @Either, though.

#8

You could define:

data SomethingElse = Either

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.

#9

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?

#10

There are a couple of issues with the code you posted:

  1. You need to give a type signature to recursor. In general, pattern matching on a GADT (such as HList) requires a type signature.
  2. 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?

1 Like
#11

I have been able to make it work like this:

{-# 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)))

Oh wow @adamgundry’s solution is much nicer:

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 ""