Pull type-level value out of dependent type/using type-level bindings at value-level

When I have a dependent type in Haskell, how do I use the value stored in the type in a function? Example Haskell program that I would want to write (which does not compile, because the min and max typelevel bindings do not extend to value level):

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
module CharRange (CharRange, ofChar, asChar) where

data CharRange :: Char -> Char -> * where
  C :: Char -> CharRange min max

ofChar :: Char -> CharRange min max
ofChar c =
  if min <= c && c <= max
  then C c
  else C min

asChar :: CharRange min max -> Char
asChar (C c) =
  if min <= c && c <= max
  then c
  else min

I can do this in Idris:

module CharRange

%default total
%access export

data CharRange : Char -> Char -> Type where
  C : Char -> CharRange min max

ofChar : Char -> CharRange min max
ofChar c =
  if min <= c && c <= max
  then C c
  else C min

asChar : CharRange min max -> Char
asChar (C c) =
  if min <= c && c <= max
  then c
  else min

Which compiles and works as expected:

λΠ> the (CharRange 'a' 'z') $ ofChar 'M'
C 'a' : CharRange 'a' 'z'
λΠ> the (CharRange 'a' 'z') $ ofChar 'm'
C 'm' : CharRange 'a' 'z'

How do I translate this Idris program to Haskell without reducing the amount of information in the type?

Solution

One possibility (however I am not convinced it is worth the trouble) is to index your CharRange with Natural numbers rather than the Char they encode.

This way you get use GHC.TypeNats to gain the ability to obtain a copy of these type levels bounds.

The worked out solution goes something like this:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Ranged (CharRange, ofChar, asChar) where

import GHC.TypeNats
import Data.Char
import Data.Proxy

data CharRange :: Nat -> Nat -> * where
  C :: Char -> CharRange min max

ofChar :: forall min max. (KnownNat min, KnownNat max)
       => Char -> CharRange min max
ofChar c =
  let min = fromIntegral $ natVal (Proxy :: Proxy min) in
  let max = fromIntegral $ natVal (Proxy :: Proxy max) in
  if min <= fromEnum c && fromEnum c <= max
  then C c
  else C (toEnum min)

asChar :: forall min max. (KnownNat min, KnownNat max)
       => CharRange min max -> Char
asChar (C c) =
  let min = fromIntegral $ natVal (Proxy :: Proxy min) in
  let max = fromIntegral $ natVal (Proxy :: Proxy max) in
  if min <= fromEnum c && fromEnum c <= max
  then c
  else toEnum min