# Do constraint checking influence typing correctness?

**URL:** <https://discourse.haskell.org/t/do-constraint-checking-influence-typing-correctness/2213>\
**Category:** Learn\
**Created:** [March 24, 2021, 7:03pm UTC](https://discourse.haskell.org/t/do-constraint-checking-influence-typing-correctness/2213 "2021-03-24T19:03:34Z")\
**Posts on this page:** 11\
**Page:** 1

<div class="post-metadata">

**Author:** ![bedlam](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/bedlam/32/1340_2.png) [@bedlam](https://discourse.haskell.org/u/bedlam)\
**Post date:** [March 24, 2021, 7:03pm UTC](https://discourse.haskell.org/t/do-constraint-checking-influence-typing-correctness/2213/1 "2021-03-24T19:03:35Z")

</div>

I have this code:

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

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [March 24, 2021, 7:11pm UTC](https://discourse.haskell.org/t/do-constraint-checking-influence-typing-correctness/2213/2 "2021-03-24T19:11:32Z")

</div>

I’m getting:

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

---

<div class="post-metadata">

**Author:** ![bedlam](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/bedlam/32/1340_2.png) [@bedlam](https://discourse.haskell.org/u/bedlam)\
**Post date:** [March 24, 2021, 7:21pm UTC](https://discourse.haskell.org/t/do-constraint-checking-influence-typing-correctness/2213/3 "2021-03-24T19:21:13Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![bedlam](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/bedlam/32/1340_2.png) [@bedlam](https://discourse.haskell.org/u/bedlam)\
**Post date:** [March 24, 2021, 7:23pm UTC](https://discourse.haskell.org/t/do-constraint-checking-influence-typing-correctness/2213/4 "2021-03-24T19:23:21Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [March 24, 2021, 7:30pm UTC](https://discourse.haskell.org/t/do-constraint-checking-influence-typing-correctness/2213/5 "2021-03-24T19:30:51Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![adamgundry](https://avatars.discourse-cdn.com/v4/letter/a/34f0e0/32.png) [@adamgundry](https://discourse.haskell.org/u/adamgundry)\
**Post date:** [March 24, 2021, 7:42pm UTC](https://discourse.haskell.org/t/do-constraint-checking-influence-typing-correctness/2213/6 "2021-03-24T19:42:49Z")

</div>

When you write this:

```haskell
_ = 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.

---

<div class="post-metadata">

**Author:** ![bedlam](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/bedlam/32/1340_2.png) [@bedlam](https://discourse.haskell.org/u/bedlam)\
**Post date:** [March 24, 2021, 7:55pm UTC](https://discourse.haskell.org/t/do-constraint-checking-influence-typing-correctness/2213/7 "2021-03-24T19:55:44Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [March 24, 2021, 9:05pm UTC](https://discourse.haskell.org/t/do-constraint-checking-influence-typing-correctness/2213/8 "2021-03-24T21:05:01Z")

</div>

> [@bedlam](#):
>
> I don’t have anything else named Either, because it would cause a compilation error, wouldn’t it?

You could define:

```haskell
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`.

> [@bedlam](#):
>
> I expect that fu can take anything, including type constructors. It still complaints about the absence of parameters with `fu @Either`, though.

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.

---

<div class="post-metadata">

**Author:** ![bedlam](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/bedlam/32/1340_2.png) [@bedlam](https://discourse.haskell.org/u/bedlam)\
**Post date:** [March 24, 2021, 9:23pm UTC](https://discourse.haskell.org/t/do-constraint-checking-influence-typing-correctness/2213/9 "2021-03-24T21:23:04Z")

</div>

Yes that was me.  
The main thing I wanted to get info about was actually about this piece:

```haskell
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?

---

<div class="post-metadata">

**Author:** ![adamgundry](https://avatars.discourse-cdn.com/v4/letter/a/34f0e0/32.png) [@adamgundry](https://discourse.haskell.org/u/adamgundry)\
**Post date:** [March 24, 2021, 10:06pm UTC](https://discourse.haskell.org/t/do-constraint-checking-influence-typing-correctness/2213/10 "2021-03-24T22:06:05Z")

</div>

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:

```haskell
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?

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [March 24, 2021, 10:12pm UTC](https://discourse.haskell.org/t/do-constraint-checking-influence-typing-correctness/2213/11 "2021-03-24T22:12:31Z")

</div>

I have been able to make it work like this:

```haskell
{-# 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:

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

```