I have a type parametrized by a natural number `n`:

```
data MyType (n :: Nat) = MyType

```

Operations on this type only make sense when `n > 0`, so I specified that as a constraint:

```
myFunction :: (KnownNat n, 1 <= n) => MyType n -> MyType n
myFunction = id

```

(Note that real versions of these functions *do* use `n` by turning it into a value with `natVal`.)

I want to create an existential type (`SomeMyType`) that lets us choose an `n` at runtime:

```
data SomeMyType where
  SomeMyType :: forall n. (KnownNat n, 1 <= n) => MyType n -> SomeMyType

```

To produce values of `SomeMyType`, I'm writing a `someMyTypeVal` function that works like `someNatVal`:

```
someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
  | n > 0 = case someNatVal n of
      Just (SomeNat (_ :: p n)) -> Just (SomeMyType (MyType @n))
      Nothing                   -> Nothing
  | otherwise = Nothing

```

This would work perfectly fine without the `1 <= n` constraint, but with the constraint I get the following type error:

```
• Couldn't match type ‘1 <=? n’ with ‘'True’
    arising from a use of ‘SomeMyType’

```

How can I get around this limitation? Since I've checked that `n > 0` at runtime, I would not mind using an operation like `unsafeCoerce` here to convince GHC that `1 <= n` is true—but I can't *just* use `unsafeCoerce` because that would lose the type-level value of `n`.

What's the best way of dealing with this?