I'm trying to define a function named `byteWidth`, which captures the usage about "get byte width of specific atomic type".

---

My 1st trial:

```
byteWidth : Type -> Int
byteWidth Int = 8
byteWidth Char = 1

```

And the Idris compiler complains: "When checking left hand side of byteWidth: No explicit types on left hand side: Int"

---

My 2nd trial:

```
interface BW a where
  byteWidth : a -> Int

implementation BW Int where
  byteWidth _ = 8

implementation BW Char where
  byteWidth _ = 1

```

And in this case, I can only use `byteWidth` like `byteWidth 'a'` but not `byteWidth Char`.