Ticket #2101 (new feature request)

Opened 9 months ago

Last modified 2 months ago

Allow some form of type-level lemma

Reported by: guest Assigned to:
Priority: normal Milestone: _|_
Component: Compiler Version: 6.8.2
Severity: normal Keywords:
Cc: ryani.spam@gmail.com Difficulty: Unknown
Test Case: Architecture: Unknown/Multiple
Operating System: Unknown/Multiple

Change History

(follow-up: ↓ 2 ) 02/15/08 16:17:10 changed by Isaac Dupree

can cat_nil already be optimized away by ghc -O? Or might it return _|_? (is it possible for its recursion not to terminate?)

(in reply to: ↑ 1 ) 02/15/08 17:36:11 changed by ryani

Replying to Isaac Dupree:

can cat_nil already be optimized away by ghc -O? Or might it return _|_? (is it possible for its recursion not to terminate?)

I am pretty sure that cat_nil cannot be optimized away. Consider the following additions to the program:

type instance Cat [a] () = [(a,a)]

unsoundCoerce :: Exp (Cat [a] ()) -> Exp [a]
unsoundCoerce = coerce undefined

If cat_nil is optimized away then unsoundCoerce exp does an invalid conversion from Exp [(a,a)] to Exp [a].

02/16/08 10:22:11 changed by igloo

  • difficulty set to Unknown.
  • milestone set to _|_.

09/30/08 08:37:27 changed by simonmar

  • architecture changed from Unknown to Unknown/Multiple.

09/30/08 08:51:41 changed by simonmar

  • os changed from Unknown to Unknown/Multiple.