dictionary: Set encoding early when cloning a dictionary.

dictionary: Set encoding early when cloning a dictionary.

Many operations that involve the names of variables and other entities
in a dictionary depend on the dictionary's encoding, so it is
potentially important to have the encoding set properly when adding
other entities to the dictionary.

I did not check that this fixes an actual bug.