Add check for inhabited datatypes

[joscoh]

Issue #, if available: #306

Description of changes:
Adds check to ensure datatypes are inhabited to ensure soundness of destructor generation
This check uses memoization to avoid repeated computation, but is conservative, rejecting types like List Empty that are inhabited.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[MikaelMayer]

This PR adds an inhabited type check for datatypes to ensure soundness of destructor generation. The implementation uses memoization to handle mutually recursive types and correctly rejects uninhabited types. The approach is conservative but sound, with excellent test coverage. Minor documentation improvements would be helpful, but the code is solid and ready to merge.

[MikaelMayer]

The termination proof uses Prod.Lex with a tuple (adts.size - seen.length, t.size). While correct, the reasoning could be documented:

Suggested change

	knowType res
	knowType res
	/--
	Termination: We use lexicographic ordering on (remaining types, type size).
	- Left component decreases when we add a type to `seen`
	- Right component decreases when we recurse into type arguments
	-/

[MikaelMayer]

The comment "Only add false if not in a cycle, it may resolve later" is subtle. Consider expanding:

    -- Only memoize 'false' if we're not in a cycle (seen.isEmpty).
    -- If we're in a cycle, the type might still be inhabited via another path,
    -- so we defer memoization until the cycle is fully explored.
    if b || seen.isEmpty then

[MikaelMayer]

Excellent test coverage

The test additions are comprehensive, covering:

• Standard inhabited types (Option, List, Either, Nat)
• Mutually recursive inhabited types (Even/Odd, Forest/Tree)
• Uninhabited types (Empty, mutually uninhabited cycles)
• Three-way cycles

This is exactly the right level of testing.