For example in the following code can I fill the hole to always compute the Nat value corresponding to the type level n parameter?
{-# LANGUAGE DataKinds, KindSignatures, ExplicitForAll #-}
data Nat
= Zero
| Succ Nat
lower :: forall (n :: Nat) . Nat
lower = _
test0 = lower @Zero == Zero
test1 = lower @(Succ Zero) == Succ Zero
I tried using a type class:
class Lower (n :: Nat) where
lower :: Nat
instance Lower Zero where
lower = Zero
instance Lower n => Lower (Succ n) where
lower = Succ (lower @n)
But then every time I want to use lower I need to explicitly require Lower n:
lower' :: forall (n :: Nat) . Lower n => Nat
lower' = lower @n
The short answer is "no".
As noted in the comments, in Haskell, type parameters are erased at runtime. What this actually means is that the runtime behavior of a function depends only on the arguments supplied for its term-level parameters, never (directly) on the arguments supplied for its type-level parameters.
Put more directly, a function is a function of its term-level parameters only, and so the value of a function application is determined by the value of the term-level arguments, irrespective of the type-level arguments. If we call the same function twice with the same term-level arguments but different type-level arguments, the two application will produce the same term-level result.
In practice, this is usually a distinction without a difference. The function:
id :: forall a. a -> a
id x = x
has runtime behavior that depends only on its term-level parameter x. If I call id True multiple times, it always produces the result True, irrespective of the type-level argument a. BUT, obviously, if the term-level argument is True, then the type-level argument is necessarily Bool, so the question of whether id True would produce the same result with different type-level arguments for parameter a is moot.
But for your example, the question is not moot. Your function:
lower :: (forall n :: Nat). Nat
must produce a value that depends only on its term-level parameters (of which there are none), and never on its type-level parameter n. Multiple calls of lower with different type-level arguments will still have the same (nullary) term-level arguments, and so the call lower must always produce the same term-level result. It is therefore impossible for lower to produce Zero for some type-level argument and Succ Zero for some other type-level argument.
A constraint is a "magical" term-level parameter. Specifically, your Lower n constraint is syntactic sugar for a newtype parameter:
newtype CLower n = CLower { lower :: Nat }
that exhibits a "coherence" property such that for each possible value for the type-level parameter n, there is only one valid term-level value of type CLower n, and Haskell will automatically supply this (only possible) term-level value wherever it is needed.
So your type-class version of lower' is roughly equivalent to:
lower' :: (forall n :: Nat). CLower n -> Nat
lower' (CLower x) = x
with the appropriate CLower n argument automatically supplied where needed.
This provides a means for the type-level parameter to come pretty close to directly determining runtime behavior. In this situation, it's still the case that lower' can only depend on its term-level parameter CLower x, but now this term-level parameter has a type (and so a value) that depends on the type-level parameter n. If you call lower' with two different type-level arguments, Haskell automatically supplies two different term-level arguments, and the result of these two lower' calls can and will return two different term-level values.
If you want to avoid a constraint and still get two different results for two different type-level arguments, you must introduce some other term-level parameter on which lower can depend. Trivially, you could write something like:
lower :: forall (n :: Nat). Int -> Nat
Now, lower has a term-level parameter (an integer), so it can produce different results for different term-level arguments:
lower 0 = Zero
lower m = Succ (lower (m-1))
This is not a very smart approach, of course, because the term-level parameter m :: Int is completely unrelated to the type-level n :: Nat parameter. If you want your term-level parameter to somehow relate to the type-level parameter n, it must have a type that depends on n, like so:
lower :: forall (n :: Nat). Something n -> Nat
and you'll need to make Something into a GADT like:
data Something n where
SZero :: Something Zero
SSucc :: Something n -> Something (Succ n)
so you can write a body for lower that acts on different term-level arguments that in turn have been determined by the type-level argument:
lower :: forall (n :: Nat). Something n -> Nat
lower (SZero) = Zero
lower (SSucc n) = Succ (lower n)
This isn't very ergonomic for your use case because when it comes time to actually invoke lower with a particular type-level argument, you need to supply the matching term-level argument explicitly:
lower @Zero SZero
or, since Haskell can infer the type-level argument automatically, just:
lower SZero
and then you have to ask yourself why not just use the term-level Zero directly, if you still need to pass a term-level SZero around to call lower.
Still, term-level parameters that take the form of either constraints or GADTs are really the only mechanism to have a type-level parameter affect the runtime behavior of a function in the way you want.