Opened 6 years ago

Last modified 6 years ago

#2101 new feature request

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 (5)

comment:1 follow-up: Changed 6 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?)

comment:2 in reply to: ↑ 1 Changed 6 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].

comment:3 Changed 6 years ago by igloo

  • Difficulty set to Unknown
  • Milestone set to _|_

comment:4 Changed 6 years ago by simonmar

  • Architecture changed from Unknown to Unknown/Multiple

comment:5 Changed 6 years ago by simonmar

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