[SOLVED] Using a type variable at the term level

Using a type variable at the term level

Consider the following GADT, Pin:

{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}

module Mcu where

import Data.Kind (Type)
import GHC.Num.Natural (Natural)

data Pin :: Natural -> Type where
  RedLED :: Pin 0
  GreenLED :: Pin 1
  Buzzer :: Pin 2

I would like to know at the term level what the type variable n (of kind Natural) is:

pinOf :: Pin n -> Natural

The following attempt:

pinOf :: Pin n -> Natural
pinOf _ = n

Results in error:

Variable not in scope: n :: Natural

Enabling ScopedTypeVariables and using forall doesn't work either:

pinOf :: forall n. Pin n -> Natural
pinOf _ = n

This results in the error:

Illegal term-level use of the type variable n

Solution

Use natVal:

{-# LANGUAGE DataKinds #-}

module Main(main) where

import Data.Kind (Type)
import GHC.TypeNats

data Pin :: Natural -> Type where
  RedLED   :: Pin 0
  GreenLED :: Pin 1
  Buzzer   :: Pin 2

pinOf :: KnownNat n => Pin n -> Natural
pinOf = natVal

main :: IO ()
main = do print (pinOf RedLED)
          print (pinOf GreenLED)
          print (pinOf Buzzer)

This prints:

0
1
2