Are Lists Inductive or Coinductive in Haskell?

Due to laziness, Haskell types are both inductive and coinductive, or, there is no formal distinguishment between data and codata. All recursive types can contain an infinite nesting of constructors. In languages such as Idris, Coq, Agda, etc. a definition like ones = 1 : ones is rejected by the termination checker. Laziness means that ones can be evaluated in one step to 1 : ones, whereas the other languages evaluate to normal form only, and ones does not have a normal form.

‘Coinductive’ does not mean ‘necessarily infinite’, it means ‘defined by how it is deconstructed’, wheras inductive means ‘defined by how it is constructed’. I think this is an excellent explanation of the subtle difference. Surely you would agree that the type

codata A : Type where MkA : A

cannot be infinite.

This is an interesting one – as opposed to HList, which you can never ‘know’ if it is finite or infinite (specifically, you can discover in finite time if a list is finite, but you can’t compute that it is infinite), HList' gives you a simple way to decide in constant time if your list is finite or infinite.