<div dir="auto"><div>Your type signature is more polykinded than your definition. Remember that</div><div dir="auto"><br></div><div dir="auto">    [] :: [a]</div><div dir="auto"><br></div><div dir="auto">or, with explicit promotion,</div><div dir="auto"><br></div><div dir="auto">    '[] :: [a]</div><div dir="auto"><br></div><div dir="auto">You write</div><div dir="auto"><br></div><div dir="auto">    x0 :: Variation ('TVariation1 :<< '[])<br>    x0 = Variation1 HNil</div><div dir="auto"><br></div><div dir="auto">Your signature more explicitly means</div><div dir="auto"><br></div><div dir="auto">    x0 :: forall a. Variation ('TVariation1 :<< ('[] :: [a]))</div><div dir="auto"><br></div><div dir="auto">But `HNil` is *not* polykinded—it can only produce HList ('[] :: [Type]).</div><div dir="auto"><br></div><div dir="auto">So you need to be a little more specific somewhere. One option:</div><div dir="auto"><br></div><div dir="auto">    data (a::k1) :<< (b::[Type])</div><div dir="auto"><br></div><div dir="auto">Another option:</div><div dir="auto"><br></div><div dir="auto">   x0 :: Variation ('TVariation1 :<< ('[] :: [Type]))<br><br><div class="gmail_quote" dir="auto"><div dir="ltr" class="gmail_attr">On Fri, Oct 22, 2021, 10:59 AM Zoran Bošnjak <<a href="mailto:zoran.bosnjak@via.si">zoran.bosnjak@via.si</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello members,<br>
I am struggling to compile the snippet below.<br>
GHC version is 8.10.4.<br>
<br>
If I try to construct the 'Variation' (with the type signature), I am getting an unexpected error.<br>
(see the comments in the code below). The error is only present if the HList is empty.<br>
I would appreciate a suggestion how to fix it.<br>
<br>
regards,<br>
Zoran<br>
<br>
---<br>
{-# LANGUAGE DataKinds #-}<br>
{-# LANGUAGE GADTs #-}<br>
{-# LANGUAGE FlexibleContexts #-}<br>
{-# LANGUAGE FlexibleInstances #-}<br>
{-# LANGUAGE TypeOperators #-}<br>
{-# LANGUAGE PolyKinds #-}<br>
<br>
module Test where<br>
<br>
import           Data.Kind<br>
<br>
data (a::k1) :<< (b::k2)<br>
infixr 5 :<<<br>
<br>
data HList (ts :: [Type]) where<br>
    HNil  :: HList '[]<br>
    HCons :: x -> HList xs -> HList (x ': xs)<br>
<br>
data TVariation = TVariation1 | TVariation2<br>
<br>
data Variation vt where<br>
    Variation1 :: HList ts -> Variation ('TVariation1 :<< ts)<br>
    Variation2 :: HList ts -> Variation ('TVariation2 :<< ts)<br>
<br>
-- This works as expected, including the explicit type signature.<br>
x1 :: Variation ('TVariation1 :<< '[()])<br>
x1 = Variation1 (HCons () HNil)<br>
<br>
-- But the following 2 cases do not work as expected.<br>
<br>
-- 1. problem:<br>
-- This 'x0' type is inferred by GHC,<br>
-- but when specified as such, it won't compile.<br>
{-<br>
    • Couldn't match type ‘k’ with ‘*’<br>
      ‘k’ is a rigid type variable bound by<br>
        the type signature for:<br>
          x0 :: forall k. Variation ('TVariation1 :<< '[])<br>
        at adhoc/test.hs:39:1-38<br>
      Expected type: Variation<br>
                       ((:<<) @TVariation @[k] 'TVariation1 ('[] @k))<br>
        Actual type: Variation<br>
                       ((:<<) @TVariation @[*] 'TVariation1 ('[] @*))<br>
    • In the expression: Variation1 HNil<br>
      In an equation for ‘x0’: x0 = Variation1 HNil<br>
    • Relevant bindings include<br>
        x0 :: Variation ('TVariation1 :<< '[])<br>
          (bound at adhoc/test.hs:40:1)<br>
-}<br>
x0 :: Variation ('TVariation1 :<< '[])<br>
x0 = Variation1 HNil<br>
<br>
class Empty t where<br>
    mkEmpty :: t<br>
<br>
-- 2. problem:<br>
-- This instance declaration reports the same problem (as in x0 above).<br>
instance Empty (Variation ('TVariation1 :<< '[])) where<br>
    mkEmpty = Variation1 HNil<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div></div></div>