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

Question

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?