unexpected compile error with wrapped HList

22 Oct 2021

      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

Zoran Bošnjak

David Feuer

tags

participants (2)