type constructor currying? (trying to create a data constructor accepting one type from another data constructor accepting two types)

Question

I'm just starting to learn Haskell, and I'm trying to put it to practice by making a card game. I'm trying to create a type "Hand" which represents a fixed sized Vector of cards (using sized vectors as described here: https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell)

I've had a few attempts at this, but none of them have worked:

{-# LANGUAGE GADTs, KindSignatures, DataKinds, PolyKinds #-}
{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}

import Data.Type.Natural
import Data.Vector.Sized (Vector)
import Card -- | I have the Card type defined in another file

data Hand (n :: Nat) where
    Hand :: SNat n -> Vector Card n

{- fails with:
* Data constructor 'Hand' returns type 'Vector Card n'
    instead of an instance of its parent type 'Hand n'
* In the definition of data constructor 'Hand'
  In the data type declaration for 'Hand'
-}

type Hand = Vector Card

{- compiles, but it doesn't work as expected:
ghci> :k Hand
Hand :: *
(whereas I'd expect 'Hand :: Nat -> Vector Card Nat' or something)
-}

I'm not really sure what to call this, it seems something like type constructor currying to me, but maybe I'm completely wrong. I haven't been able to find something similar online. Thanks in advance for the help!

Answer 1

Vector from Data.Vector.Sized takes the size as the first argument, not the second, unlike in the linked tutorial. So you need

type Hand n = Vector n Card

As for your GADT variant, you are simply missing the result type of the constructor.

data Hand (n :: Nat) where
    Hand :: SNat n -> Vector n Card -> Hand n
                                   ^^^^^^^^^^

GADT constructor types always need a codomain of whatever type they are defining. That said, I think the SNat here is unnecessary -- if the information of how many cards are in the hand comes from outside, there's no reason to hold onto it inside also.