Q:

Wellsortedness error ... not of sort equal

Here is a trivial translator from language foo to bar:
type_synonym vname = "string"
type_synonym 'a env = "vname ⇒ 'a option"

datatype foo_exp = FooBConst bool
datatype foo_type = FooBType | FooIType | FooSType

datatype bar_exp = BarBConst bool
datatype bar_type = BarBType | BarIType

fun foo_to_bar_type :: "foo_type ⇒ bar_type option" where
  "foo_to_bar_type FooBType = Some BarBType" |
  "foo_to_bar_type FooIType = Some BarIType" |
  "foo_to_bar_type _ = None"

inductive foo_to_bar :: "foo_type env ⇒ foo_exp ⇒ bar_type env ⇒ bar_exp ⇒ bool" where
"Γ⇩B = map_comp foo_to_bar_type Γ⇩F ⟹
 foo_to_bar Γ⇩F (FooBConst c) Γ⇩B (BarBConst c)"

code_pred [show_modes] foo_to_bar . 

values "{t. foo_to_bar Map.empty (FooBConst True) Map.empty t}"

The last line causes the following error:
Wellsortedness error
(in code equation foo_to_bar_i_i_i_o ? x ? xa ? xb ≡
                  Predicate.bind (Predicate.single (? x, ? xa, ? xb))
                   (λ(Γ⇩F_, aa, Γ⇩B_). 
                       case aa of
                       FooBConst c_ ⇒
                         Predicate.bind (eq_i_i Γ⇩B_ (foo_to_bar_type ∘⇩m Γ⇩F_))
                          (λ().  Predicate.single (BarBConst c_))),
with dependency "Pure.dummy_pattern" -> "foo_to_bar_i_i_i_o"):
Type char list ⇒ bar_type option not of sort equal
No type arity list :: enum

Could you suggest me how to fix it? 
Also foo_to_bar has mode i => i => o => o => boolpos.  How should I execute values to generate both 3rd and 4th arguments? 

A:

In general I'd advise against using inductive to define something that can easily be expressed as a function.  While the predicate compiler comes with a lot of bells and whistles to make computational sense of an inductive definition, there are a lot of problems that can arise because it's so complex.  In your case, the problem lies in the line
Γ⇩B = map_comp foo_to_bar_type Γ⇩F

You are trying to compare two functions.  The predicate compiler doesn't know that it can be seen as a "defining equation".  In a sense, you're asking the predicate compiler to solve an impossible problem. 
Your life will be much easier if foo_to_bar is defined as a function (or plain definition) instead.  It'll work out of the box with the code generator.