[Haskell-cafe] unexpected compile error with wrapped HList

[David Feuer]

Your type signature is more polykinded than your definition. Remember that

    [] :: [a]

or, with explicit promotion,

    '[] :: [a]

You write

    x0 :: Variation ('TVariation1 :<< '[])
    x0 = Variation1 HNil

Your signature more explicitly means

    x0 :: forall a. Variation ('TVariation1 :<< ('[] :: [a]))

But `HNil` is *not* polykinded—it can only produce HList ('[] :: [Type]).

So you need to be a little more specific somewhere. One option:

    data (a::k1) :<< (b::[Type])

Another option:

   x0 :: Variation ('TVariation1 :<< ('[] :: [Type]))

On Fri, Oct 22, 2021, 10:59 AM Zoran Bošnjak <zoran.bosnjak at via.si> wrote:

> Hello members,
> I am struggling to compile the snippet below.
> GHC version is 8.10.4.
>
> If I try to construct the 'Variation' (with the type signature), I am
> getting an unexpected error.
> (see the comments in the code below). The error is only present if the
> HList is empty.
> I would appreciate a suggestion how to fix it.
>
> regards,
> Zoran
>
> ---
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE FlexibleContexts #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE PolyKinds #-}
>
> module Test where
>
> import           Data.Kind
>
> data (a::k1) :<< (b::k2)
> infixr 5 :<<
>
> data HList (ts :: [Type]) where
>     HNil  :: HList '[]
>     HCons :: x -> HList xs -> HList (x ': xs)
>
> data TVariation = TVariation1 | TVariation2
>
> data Variation vt where
>     Variation1 :: HList ts -> Variation ('TVariation1 :<< ts)
>     Variation2 :: HList ts -> Variation ('TVariation2 :<< ts)
>
> -- This works as expected, including the explicit type signature.
> x1 :: Variation ('TVariation1 :<< '[()])
> x1 = Variation1 (HCons () HNil)
>
> -- But the following 2 cases do not work as expected.
>
> -- 1. problem:
> -- This 'x0' type is inferred by GHC,
> -- but when specified as such, it won't compile.
> {-
>     • Couldn't match type ‘k’ with ‘*’
>       ‘k’ is a rigid type variable bound by
>         the type signature for:
>           x0 :: forall k. Variation ('TVariation1 :<< '[])
>         at adhoc/test.hs:39:1-38
>       Expected type: Variation
>                        ((:<<) @TVariation @[k] 'TVariation1 ('[] @k))
>         Actual type: Variation
>                        ((:<<) @TVariation @[*] 'TVariation1 ('[] @*))
>     • In the expression: Variation1 HNil
>       In an equation for ‘x0’: x0 = Variation1 HNil
>     • Relevant bindings include
>         x0 :: Variation ('TVariation1 :<< '[])
>           (bound at adhoc/test.hs:40:1)
> -}
> x0 :: Variation ('TVariation1 :<< '[])
> x0 = Variation1 HNil
>
> class Empty t where
>     mkEmpty :: t
>
> -- 2. problem:
> -- This instance declaration reports the same problem (as in x0 above).
> instance Empty (Variation ('TVariation1 :<< '[])) where
>     mkEmpty = Variation1 HNil
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20211022/0dbaa178/attachment.html>