Add tests for default implict record type arguments

tests/idris2/record003/Record.idr

@@ -14,3 +14,20 @@ b = Check
 {- Will not type-check
 c : Positive 0
 -}
+
+data KindOfString = ASCII | UTF
+
+UTForASCII : KindOfString -> Type
+UTForASCII UTF = String
+UTForASCII ASCII = List Char   --- Just to demonstrate
+
+record FlexiString { default UTF k : KindOfString} where
+  constructor MkFlexiString
+  val : UTForASCII k
+  
+c : FlexiString
+c = MkFlexiString "hello"
+
+d : FlexiString {k = ASCII}
+d = MkFlexiString ['h', 'i']
+

tests/ttimp/record003/Record.yaff

@@ -14,3 +14,22 @@ a = Check
 b : Positive (S (S Z))
 b = Check
 
+
+data KindOfString : Type where
+ ASCII : KindOfString
+ UTF   : KindOfString
+
+UTForASCII : KindOfString -> Type
+UTForASCII UTF = String
+UTForASCII ASCII = Nat   -- Just as demonstration
+
+record FlexiString { default UTF k : KindOfString} where
+  constructor MkFlexiString
+  val : UTForASCII k
+  
+c : FlexiString
+c = MkFlexiString "hello"
+
+d : FlexiString {k = ASCII}
+d = MkFlexiString Z
+

tests/ttimp/record003/run

@@ -1,4 +1,4 @@
-$1 --yaffle Record.yaff -c < input
+$1 --yaffle Record.yaff          < input
 $1 --yaffle build/ttc/Record.ttc < input
 
 rm -rf build