foo.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Lib where

import Data.Char

someFunc :: IO ()
someFunc = putStrLn "someFunc"

data SNat where
  SZ :: SNat
  SS :: SNat -> SNat

type family TensorRank (n :: SNat) a :: * where
  TensorRank SZ a = a
  TensorRank (SS k) a = TensorRank k [a]

dec1 :: TensorRank SZ Char -> Int
dec1 k = ord k -- accepts that TensorRank SZ Char is Char

dec2 :: TensorRank (SS SZ) Char -> Int
dec2 k = length k -- accepts that TensorRank (SS SZ) Char is [Char]

dec3 :: TensorRank (SS(SS SZ)) Char -> Int
dec3 k = _dsfd3 -- Hole

-- Is there a way to have TensorRank ('SS ('SS 'SZ)) Char in the hole below
-- reduce to [[Char]] in the binding for k? I'd like to make a hole and see it
-- say [[Char]], having to apply the type family in my own head while
-- examining a context is burdensome. Is this an issue I've caused with
-- UndecidableInstances above? I'm not sure how to write TensorRank without it.

{-

Lib.hs:36:10-15:
error:
    • Found hole: _dsfd3 :: Int
      Or perhaps ‘_dsfd3’ is mis-spelled, or not in scope
    • In the expression: _dsfd3
      In an equation for ‘dec3’: dec3 k = _dsfd3
    • Relevant bindings include
        k :: TensorRank ('SS ('SS 'SZ)) Char
          (bound at /media/storage/home/august/projects/hsprojects/tenso/src/Lib.hs:36:6)
        dec3 :: TensorRank ('SS ('SS 'SZ)) Char -> Int
          (bound at /media/storage/home/august/projects/hsprojects/tenso/src/Lib.hs:36:1)

-}