[ fix #3669 ] Fix missing handling of dotted patterns (#3671)

* [ fix #3669 ] Handle dotted in `findUsed`

* [ fix ] Fix comparing `Dotted` types in `CaseBuilder`

* [ fix ] Handle `IMustUnify` in `mkTerm`

* [ admin ] Update CHANGELOG

---------

Co-authored-by: CodingCellist <[email protected]>

Author: spcfox

CHANGELOG_NEXT.md

@@ -9,6 +9,9 @@ should target this file (`CHANGELOG_NEXT`).
 
 ### Compiler changes
 
+* Fixed missing handling of dotted patterns See
+  [#3669](https://github.com/idris-lang/Idris2/issues/3669),
+  [comment](https://github.com/idris-lang/Idris2/issues/3644#issuecomment-3286320272).
 * Removed modules and functions moved to `base`:
   - `Libraries.Data.Fin` → `Data.Fin`
   - `Libraries.Data.IOArray` → `Data.IOArray`
@@ -22,7 +25,6 @@ should target this file (`CHANGELOG_NEXT`).
   - `Libraries.Data.SortedMap` → `Data.SortedMap`
   - `Libraries.Data.SortedSet` → `Data.SortedSet`
   - `Libraries.Utils.Binary.bufferData'` → `Data.Buffer.bufferData'`
-
 * Removed unused functions:
   - `Libraries.Data.List.Extra`: `breakAfter`, `splitAfter` and `zipMaybe`
   - `Libraries.Data.List.Quantifiers.Extra.tabulate`.

src/Core/Case/CaseBuilder.idr

@@ -798,6 +798,8 @@ sameType {ns} fc phase fn env (p :: xs)
     headEq (NPrimVal _ c) (NPrimVal _ c') _ = c == c'
     headEq (NType {}) (NType {}) _ = True
     headEq (NApp _ (NRef _ n) _) (NApp _ (NRef _ n') _) RunTime = n == n'
+    headEq (NErased _ (Dotted x)) y ph = headEq x y ph
+    headEq x (NErased _ (Dotted y)) ph = headEq x y ph
     headEq (NErased {}) _ RunTime = True
     headEq _ (NErased {}) RunTime = True
     headEq _ _ _ = False

src/Core/Env.idr

@@ -221,6 +221,8 @@ mutual
       = findUsed env (findUsed env used ty) tm
   findUsed env used (TForce fc r tm)
       = findUsed env used tm
+  findUsed env used (Erased fc (Dotted tm))
+      = findUsed env used tm
   findUsed env used _ = used
 
   findUsedInBinder : {vars : _} ->

src/TTImp/Impossible.idr

@@ -162,6 +162,8 @@ mutual
      = mkTerm fn mty exps (arg :: autos) named
   mkTerm (INamedApp fc fn nm arg) mty exps autos named
      = mkTerm fn mty exps autos ((nm, arg) :: named)
+  mkTerm (IMustUnify fc r tm) mty exps autos named
+     = Erased fc . Dotted <$> mkTerm tm mty exps autos named
   mkTerm (IPrimVal fc c) _ _ _ _ = pure (PrimVal fc c)
   mkTerm (IAlternative _ (UniqueDefault tm) _) mty exps autos named
      = mkTerm tm mty exps autos named

tests/idris2/basic/dotted002/DottedType.idr

@@ -0,0 +1,6 @@
+data Identity : Type -> Type where
+  MkIdentity : (a : Type) -> a -> Identity a
+
+foo : Identity Bool -> ()
+foo (MkIdentity .(Bool) True)  = ()
+foo (MkIdentity .(Bool) False) = ()

tests/idris2/basic/dotted002/expected

@@ -0,0 +1 @@
+1/1: Building DottedType (DottedType.idr)

tests/idris2/basic/dotted002/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check DottedType.idr

tests/idris2/coverage/impossible001/DottedTypeImpossible.idr

@@ -0,0 +1,6 @@
+data Identity : Type -> Type where
+  MkIdentity : (a : Type) -> a -> Identity a
+
+foo : Identity Bool -> Void -> ()
+foo (MkIdentity .(Bool) True)  _ impossible
+foo (MkIdentity .(Bool) False) _ impossible

tests/idris2/coverage/impossible001/expected

@@ -0,0 +1 @@
+1/1: Building DottedTypeImpossible (DottedTypeImpossible.idr)

tests/idris2/coverage/impossible001/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check DottedTypeImpossible.idr