Ticket #2101 (new feature request)

Opened 5 years ago

Last modified 5 years ago

Allow some form of type-level lemma

Reported by: guest Owned by:
Priority: normal Milestone: _|_
Component: Compiler Version: 6.8.2
Keywords: Cc: ryani.spam@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:

Change History

follow-up: ↓ 2   Changed 5 years ago 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   Changed 5 years ago 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].

  Changed 5 years ago by igloo

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

  Changed 5 years ago by simonmar

  • architecture changed from Unknown to Unknown/Multiple

  Changed 5 years ago by simonmar

  • os changed from Unknown to Unknown/Multiple
Note: See TracTickets for help on using tickets.