Ungrounded record error when destructuring with don't-cares?

[TomBinford]

Hi,
I'm attempting to "destructure" records using = so that I can get arguments for both the overall record and its fields. But I'm encountering "Error: Ungrounded record ..." with the following:

.type Type = [a: symbol, b: symbol]

.decl fact(t: Type)
fact(["abc", "xyz"]).

.decl pred(t: Type, ta: symbol)
pred(t, ta) :- fact(t), t=[ta, _].

Error: Ungrounded record in file ungrounded-record.dl at line 7
pred(t, ta) :- fact(t), t=[ta, _].
--------------------------^--------

And interestingly just avoiding _ fixes it, even though I make no use of the new variable:

- pred(t, ta) :- fact(t), t=[ta, _].
+ pred(t, ta) :- fact(t), t=[ta, _tb].

I could do this, but my real code has more don't-cares and I don't want the noise.
Could anyone please explain? Appreciate it.

[quentin]

Hi,

After the ResolveAliasesTransformer, all occurences of t are replaced with [ta,_], and the groundedness constraint system cannot give a bounded value to [ta,_] in the head (var([ta,_])->0 in the Solution).

Clause: pred([ta,_],ta) :-                                                                                                                                                                                                                                    
   fact([ta,_]).                                                                                                                                                                                                                                              
Problem:                                                                                                                                                                                                                                                      
{                                                                                                                                                                                                                                                             
        var([ta,_]) ⇒ var(ta),                                 
        var([ta,_]) ⇒ var(_),                                  
        var(ta) ∧ var(_) ⇒ var([ta,_]),
        var([ta,_]) is true,                                   
        var([ta,_]) ⇒ var(ta),                                 
        var([ta,_]) ⇒ var(_),                                  
        var(ta) ∧ var(_) ⇒ var([ta,_])
}                                                              
Solution:                                                      
{var(_)->1,var(_)->0,var([ta,_])->1,var([ta,_])->0,var(ta)->1}

When you provide an explicit variable for the second part of the record, the constraint system can be solved because the second member of the record has is bound by the variable (var(_fix)->1 and var([ta,_fix])->1):

Clause: pred([ta,_fix],ta) :- 
   fact([ta,_fix]).
Problem:
{
        var([ta,_fix]) ⇒ var(ta),
        var([ta,_fix]) ⇒ var(_fix),
        var(ta) ∧ var(_fix) ⇒ var([ta,_fix]),
        var([ta,_fix]) is true,
        var([ta,_fix]) ⇒ var(ta),
        var([ta,_fix]) ⇒ var(_fix),
        var(ta) ∧ var(_fix) ⇒ var([ta,_fix])
}
Solution:
{var([ta,_fix])->1,var([ta,_fix])->1,var(ta)->1,var(_fix)->1}

To fix this, we need to transform _ into unique variables before the ResolveAliasesTransformer.