From f189e916290fb6e3151bd3039a862d0ba9544043 Mon Sep 17 00:00:00 2001
From: "john.j.camilleri" <john.j.camilleri@chalmers.se>
Date: Wed, 2 Jul 2014 06:37:27 +0000
Subject: [PATCH] Add Nothing' to Maybe.gf, including warning

---
 lib/src/prelude/Maybe.gf | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/lib/src/prelude/Maybe.gf b/lib/src/prelude/Maybe.gf
index f2ea1bd00..e892958ff 100644
--- a/lib/src/prelude/Maybe.gf
+++ b/lib/src/prelude/Maybe.gf
@@ -9,21 +9,27 @@ resource Maybe = open Prelude, Predef in {
     -- Constructors
     Maybe   : (t : Type) -> Type = \t -> {
       inner : t ;
-      exists : Bool
+      exists : Bool ;
       } ;
     Just    : (T : Type) -> T -> Maybe T = \_,t -> {
       inner = t ;
-      exists = True
+      exists = True ;
       } ;
-    -- Nothing : (T : Type) -> Maybe T = \_ -> {
-    --   inner = variants {} ;
-    --   exists = False
-    --   } ;
     Nothing : (T : Type) -> T -> Maybe T = \_,t -> {
       inner = t ;
-      exists = False
+      exists = False ;
       } ;
 
+    -- IMPORTANT
+    -- This version of Nothing would be preferred, but it may not work as expected.
+    -- This happens when using Nothing within a record. For discussion of this see:
+    -- https://groups.google.com/d/msg/gf-dev/KAQEttN-0Cs/EjGHjOXEKO0J
+    Nothing' : (T : Type) -> Maybe T = \_ -> {
+      inner = variants {} ;
+      exists = False ;
+      } ;
+    -- You have been warned!
+
     -- Functions
     exists   : (T : Type) -> Maybe T -> Bool = \_,m -> m.exists ;
     isJust   : (T : Type) -> Maybe T -> Bool = \_,m -> m.exists ;