Passing -fdefer-type-errors to GHC causes confusing errors from LH

[matthew-healy]

While implementing head'' in Tutorial_04_Polymorphism I made the following small typo:

head'' :: Vector a -> Maybe a
head'' v | lengt v > 0 = Just (v ! 0)
         | otherwise   = Nothing

(Note the misspelling of length as lengt). Rather than a standard "name not in scope" error, this led to the following error:

**** LIQUID: SAFE (59 constraints checked) *************************************
[ 5 of 13] Compiling Tutorial_04_Polymorphism

**** LIQUID: ERROR :1:1-1:1: Error
  elaborate solver elabBE 167 "lq_anf$##7205759403792825397##d8gR" {lq_tmp$x##1261 : (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)) | [(lq_tmp$x##1261 = lq_anf$##7205759403792825396##d8gQ)]} failed on:
      lq_tmp$x##1261 == lq_anf$##7205759403792825396##d8gQ
  with error
      The sort (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)) is not numeric
  because
Cannot unify (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)) with int in expression: lq_tmp$x##1261 == lq_anf$##7205759403792825396##d8gQ 
  because
Elaborate fails on lq_tmp$x##1261 == lq_anf$##7205759403792825396##d8gQ
  in environment
      lq_anf$##7205759403792825396##d8gQ := int

      lq_tmp$x##1261 := (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)) 

After some investigation, I narrowed the cause down to the fact that -fdefer-type-errors is passed to GHC as part of building the tutorial project. Is this flag still necessary? I seem to have no major issues building the tutorial without passing that argument, and removing it results in the expected GHC error message being raised.

[mgritter]

I ran into this problem during the tutorial too -- due to a missing pair of parentheses -- and removing -fdefer-type-errors quickly clarified what the problem was. Without this change, I got the extremely confusing message in part 2:

**** LIQUID: ERROR :1:1-1:1: Error
  elaborate solver elabBE 294 "lq_anf$##7205759403792806839##d3rx" {lq_tmp$x##1878 : (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)) | [(lq_tmp$x##1878 = lq_anf$##7205759403792806838##d3rw);
                                                                         (lq_tmp$x##1878 = (GHC.Num.fromInteger lq_anf$##7205759403792806838##d3rw));
                                                                         (lq_tmp$x##1878 = (GHC.Num.fromInteger lq_anf$##7205759403792806838##d3rw))]} failed on:
      ((lq_tmp$x##1878 == lq_anf$##7205759403792806838##d3rw
        && lq_tmp$x##1878 == GHC.Num.fromInteger lq_anf$##7205759403792806838##d3rw)
       && lq_tmp$x##1878 == GHC.Num.fromInteger lq_anf$##7205759403792806838##d3rw)
  with error
      The sort (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)) is not numeric
  because
Cannot unify (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)) with int in expression: lq_tmp$x##1878 == lq_anf$##7205759403792806838##d3rw 
  because
Elaborate fails on lq_tmp$x##1878 == lq_anf$##7205759403792806838##d3rw
  in environment
      GHC.Num.fromInteger := func(1 , [int; @(0)])

      lq_anf$##7205759403792806838##d3rw := int

      lq_tmp$x##1878 := (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)) 

[ranjitjhala]

Wow thanks for catching this Mark! I think we should totally remove that flag (tbh can’t recall why it was put in in the first place!)

[matthew-healy]

@ranjitjhala I opened #120 a while ago to fix this. As far as I can tell removing the flag doesn't have any impact on the tutorial whatsoever.