Weird continuation fuckery confuses the optimiser

[plt-amy]

I was implementing the law of excluded middle, and noticed that the optimiser was removing the error from absurd, thus breaking type safety.

let lem : forall 'a. trivial => cont (either 'a ('a -> cont void)) =
  call_cc (fun not_lem -> pure (Right (fun c -> not_lem (Left c))))

let foo : either int (int -> void) =
  match run_cont lem (fun x -> x) with
  | Left i -> Left i
  | Right c -> Right (fun i -> abort (c i))

let Right k = foo

> :t k 10
void
> k 10
Left 10

Core Lint says:

amc: Core lint failed after `Reduce` with 1 errors
[...]
  in (* XXX Expected type int#t-2 -> void#t36
                 got type int#t-2 -> either#t47 int#t-2 (int#t-2 -> cont#t3 void#t36) *)
  let atp#v1211 : int#t-2 -> void#t36 =
[...]

Don't do classical logic, kids.

[Lemmmy]

My name is trademarked

[plt-amy]

That's why I'm using not_lem instead

[plt-amy]

when amulet compiles a program that GHC rejects