Re: [Haskell-cafe] unexpected compile error with wrapped HList

22 Oct 2021

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

Re: [Haskell-cafe] unexpected compile error with wrapped HList

David Feuer