# JType::not-a-type


**Key:** `JType::not-a-type`

**Category:** sort · **Severity:** error

**Source:** [`src/diag/hints.nix:870`](https://github.com/kleisli-io/nix-effects/blob/main/src/diag/hints.nix#L870)

the type parameter of `J` must be a type (live in some U(k)), not a term. Pass a type expression like `nat`, `u 0`, or the type shared by J's two endpoints.

## Example

`Hint::JType::not-a-type` means the `JType` position uses a term or value where the checker needs a type. The example shows the failing form first, then one way to give the checker the missing structure.

```nix
# Bad: J's type argument is a term.
J (natLit 0) motive refl x y p

# Better: J's type argument is the type of both endpoints.
J nat motive refl x y p

```


---

[← All diagnostic hints](/nix-effects/diag-hints)