1--
2-- Copyright 2016, NICTA
3--
4-- This software may be distributed and modified according to the terms of
5-- the GNU General Public License version 2. Note that NO WARRANTY is provided.
6-- See "LICENSE_GPLv2.txt" for details.
7--
8-- @TAG(NICTA_GPL)
9--
10
11type X
12type A
13type O = { f : X, g : U64 }
14type F = {
15    a : A,
16    o : O
17}
18type F' = {
19    a : A,
20    o : O take (f)
21}
22
23freeX: (X) -> ()
24
25bar : F -> F'
26bar(val {o}) =
27  let o {f} = o
28  and _ = freeX(f)
29  in (val {o})
30