User : { Type : Type
       , default : { mastodon : ∀(A : Type) → Optional A, name : Text }
       }

Error: Expression doesn't match annotation

{ + preferred_language : …
, …
}

Explanation: You can annotate an expression with its type or kind using the
❰:❱ symbol, like this:


    ┌───────┐
    │ x : t │  ❰x❱ is an expression and ❰t❱ is the annotated type or kind of ❰x❱
    └───────┘

The type checker verifies that the expression's type or kind matches the
provided annotation

For example, all of the following are valid annotations that the type checker
accepts:


    ┌─────────────┐
    │ 1 : Natural │  ❰1❱ is an expression that has type ❰Natural❱, so the type
    └─────────────┘  checker accepts the annotation


    ┌───────────────────────┐
    │ Natural/even 2 : Bool │  ❰Natural/even 2❱ has type ❰Bool❱, so the type
    └───────────────────────┘  checker accepts the annotation


    ┌────────────────────┐
    │ List : Type → Type │  ❰List❱ is an expression that has kind ❰Type → Type❱,
    └────────────────────┘  so the type checker accepts the annotation


    ┌──────────────────┐
    │ List Text : Type │  ❰List Text❱ is an expression that has kind ❰Type❱, so
    └──────────────────┘  the type checker accepts the annotation


However, the following annotations are not valid and the type checker will
reject them:


    ┌──────────┐
    │ 1 : Text │  The type checker rejects this because ❰1❱ does not have type
    └──────────┘  ❰Text❱


    ┌─────────────┐
    │ List : Type │  ❰List❱ does not have kind ❰Type❱
    └─────────────┘


Some common reasons why you might get this error:

● The Haskell Dhall interpreter implicitly inserts a top-level annotation
  matching the expected type

  For example, if you run the following Haskell code:


    ┌───────────────────────────────┐
    │ >>> input auto "1" :: IO Text │
    └───────────────────────────────┘


  ... then the interpreter will actually type check the following annotated
  expression:


    ┌──────────┐
    │ 1 : Text │
    └──────────┘


  ... and then type-checking will fail

────────────────────────────────────────────────────────────────────────────────

You or the interpreter annotated this expression:

↳   User.default
  ⫽ { name = "Cadey"
    , mastodon = Some "@cadey@mst3k.interlinked.me"
    , preferred_language = "en-US"
    }

... with this type or kind:

↳ { mastodon : Optional Text, name : Text }

... but the inferred type or kind of the expression is actually:

↳ { mastodon : Optional Text, name : Text, preferred_language : Text }

────────────────────────────────────────────────────────────────────────────────

4│         User::{ name = "Cadey", mastodon = Some "@cadey@mst3k.interlinked.me",
5│       preferred_language = "en-US" }

example.dhall:4:9